1stexg - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > 1stexg		GIF version

Theorem 1stexg 6391

Description: Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.)

**Assertion**
Ref	Expression
1stexg	⊢ (𝐴 ∈ 𝑉 → (1^st ‘𝐴) ∈ V)

**Proof of Theorem 1stexg**
Step	Hyp	Ref	Expression
1		elex 2833	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		fo1st 6381	. . . 4 ⊢ 1^st :V–onto→V
3		fofn 5612	. . . 4 ⊢ (1^st :V–onto→V → 1^st Fn V)
4	2, 3	ax-mp 5	. . 3 ⊢ 1^st Fn V
5		funfvex 5707	. . . 4 ⊢ ((Fun 1^st ∧ 𝐴 ∈ dom 1^st ) → (1^st ‘𝐴) ∈ V)
6	5	funfni 5478	. . 3 ⊢ ((1^st Fn V ∧ 𝐴 ∈ V) → (1^st ‘𝐴) ∈ V)
7	4, 6	mpan 428	. 2 ⊢ (𝐴 ∈ V → (1^st ‘𝐴) ∈ V)
8	1, 7	syl 14	1 ⊢ (𝐴 ∈ 𝑉 → (1^st ‘𝐴) ∈ V)

Colors of variables: wff set class

Syntax hints: → wi 4 ∈ wcel 2209 Vcvv 2821 Fn wfn 5367 –onto→wfo 5370 ‘cfv 5372 1^st c1st 6362

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4244 ax-pow 4306 ax-pr 4341 ax-un 4573

This theorem depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533 df-rex 2534 df-v 2823 df-sbc 3052 df-un 3224 df-in 3226 df-ss 3233 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-br 4126 df-opab 4188 df-mpt 4189 df-id 4433 df-xp 4775 df-rel 4776 df-cnv 4777 df-co 4778 df-dm 4779 df-rn 4780 df-iota 5332 df-fun 5374 df-fn 5375 df-f 5376 df-fo 5378 df-fv 5380 df-1st 6364

This theorem is referenced by: elxp7 6394 xpopth 6400 eqop 6401 2nd1st 6404 2ndrn 6407 releldm2 6409 reldm 6410 dfoprab3 6415 elopabi 6421 mpofvex 6431 dfmpo 6449 cnvf1olem 6450 cnvoprab 6460 f1od2 6461 disjxp1 6462 elmpom 6464 xpmapenlem 7139 cnref1o 10030 fsumcnv 12182 fprodcnv 12370 qredeu 12853 qnumval 12941 xpsff1o 13647 txbas 15282 txdis 15301 vtxvalg 16171 vtxex 16173 wlkelvv 16504 wlk2f 16506