exim - brismu bridi

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

Theorem exim 426

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 418	. 2 ⊢ ganai su'o da zo'u brode gi ro da zo'u su'o da zo'u brode
3		wit 423	. . . 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 425	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 414

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 418 ax-eq 420

This theorem depends on definitions: df-go 83

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

W3C validator