exim - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > exim

Theorem exim 427

Description: Internalization of the concept that, if an arrow is inhabited for all values of some variable, then the existence of an inhabitant in the source of the arrow implies an inhabitant in the target of the arrow. (Contributed by la korvo, 9-Jul-2025.)

**Assertion**
Ref	Expression
exim	⊢ ganai ro da zo'u ganai broda gi brode gi ganai su'o da zo'u broda gi su'o da zo'u brode

**Proof of Theorem exim**
Step	Hyp	Ref	Expression
1		ax-ro1-nf 249	. 2 ⊢ ganai ro da zo'u ganai broda gi brode gi ro da zo'u ro da zo'u ganai broda gi brode
2		ax-eb 419	. 2 ⊢ ganai su'o da zo'u brode gi ro da zo'u su'o da zo'u brode
3		wit 424	. . . 4 ⊢ ganai brode gi su'o da zo'u brode
4	3	ganai-comp-rli 17	. . 3 ⊢ ganai ganai broda gi brode gi ganai broda gi su'o da zo'u brode
5	4	spec1s 231	. 2 ⊢ ganai ro da zo'u ganai broda gi brode gi ganai broda gi su'o da zo'u brode
6	1, 2, 5	exlimdh 426	1 ⊢ ganai ro da zo'u ganai broda gi brode gi ganai su'o da zo'u broda gi su'o da zo'u brode

Colors of variables: sumti selbri bridi

Syntax hints: ganai bgan 9 ro brd 222 su'o bsd 415

This theorem was proved from axioms: ax-mp 10 ax-k 11 ax-s 15 ax-ge-le 48 ax-ge-re 49 ax-ge-in 50 ax-gen1 224 ax-spec1 228 ax-qi1 234 ax-ro1-nf 249 ax-eb 419 ax-eq 421

This theorem depends on definitions: df-go 83

This theorem is referenced by: eximi 428 eximdh 429 foml19.29 430

W3C validator