exim - brismu bridi

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

Theorem exim 428

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

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

This theorem depends on definitions: df-go 83

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

W3C validator