1stexg - Intuitionistic Logic Explorer

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

Theorem 1stexg 6339

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 2815	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		fo1st 6329	. . . 4 ⊢ 1^st :V–onto→V
3		fofn 5570	. . . 4 ⊢ (1^st :V–onto→V → 1^st Fn V)
4	2, 3	ax-mp 5	. . 3 ⊢ 1^st Fn V
5		funfvex 5665	. . . 4 ⊢ ((Fun 1^st ∧ 𝐴 ∈ dom 1^st ) → (1^st ‘𝐴) ∈ V)
6	5	funfni 5439	. . 3 ⊢ ((1^st Fn V ∧ 𝐴 ∈ V) → (1^st ‘𝐴) ∈ V)
7	4, 6	mpan 424	. 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 2202 Vcvv 2803 Fn wfn 5328 –onto→wfo 5331 ‘cfv 5333 1^st c1st 6310

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 717 ax-5 1496 ax-7 1497 ax-gen 1498 ax-ie1 1542 ax-ie2 1543 ax-8 1553 ax-10 1554 ax-11 1555 ax-i12 1556 ax-bndl 1558 ax-4 1559 ax-17 1575 ax-i9 1579 ax-ial 1583 ax-i5r 1584 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4212 ax-pow 4270 ax-pr 4305 ax-un 4536

This theorem depends on definitions: df-bi 117 df-3an 1007 df-tru 1401 df-nf 1510 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2364 df-ral 2516 df-rex 2517 df-v 2805 df-sbc 3033 df-un 3205 df-in 3207 df-ss 3214 df-pw 3658 df-sn 3679 df-pr 3680 df-op 3682 df-uni 3899 df-br 4094 df-opab 4156 df-mpt 4157 df-id 4396 df-xp 4737 df-rel 4738 df-cnv 4739 df-co 4740 df-dm 4741 df-rn 4742 df-iota 5293 df-fun 5335 df-fn 5336 df-f 5337 df-fo 5339 df-fv 5341 df-1st 6312

This theorem is referenced by: elxp7 6342 xpopth 6348 eqop 6349 2nd1st 6352 2ndrn 6355 releldm2 6357 reldm 6358 dfoprab3 6363 elopabi 6369 mpofvex 6379 dfmpo 6397 cnvf1olem 6398 cnvoprab 6408 f1od2 6409 disjxp1 6410 elmpom 6412 xpmapenlem 7078 cnref1o 9946 fsumcnv 12078 fprodcnv 12266 qredeu 12749 qnumval 12837 xpsff1o 13512 txbas 15069 txdis 15088 vtxvalg 15957 vtxex 15959 wlkelvv 16290 wlk2f 16292