1stexg - Intuitionistic Logic Explorer

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

Theorem 1stexg 6329

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 2814	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		fo1st 6319	. . . 4 ⊢ 1^st :V–onto→V
3		fofn 5561	. . . 4 ⊢ (1^st :V–onto→V → 1^st Fn V)
4	2, 3	ax-mp 5	. . 3 ⊢ 1^st Fn V
5		funfvex 5656	. . . 4 ⊢ ((Fun 1^st ∧ 𝐴 ∈ dom 1^st ) → (1^st ‘𝐴) ∈ V)
6	5	funfni 5432	. . 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 2802 Fn wfn 5321 –onto→wfo 5324 ‘cfv 5326 1^st c1st 6300

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 716 ax-5 1495 ax-7 1496 ax-gen 1497 ax-ie1 1541 ax-ie2 1542 ax-8 1552 ax-10 1553 ax-11 1554 ax-i12 1555 ax-bndl 1557 ax-4 1558 ax-17 1574 ax-i9 1578 ax-ial 1582 ax-i5r 1583 ax-13 2204 ax-14 2205 ax-ext 2213 ax-sep 4207 ax-pow 4264 ax-pr 4299 ax-un 4530

This theorem depends on definitions: df-bi 117 df-3an 1006 df-tru 1400 df-nf 1509 df-sb 1811 df-eu 2082 df-mo 2083 df-clab 2218 df-cleq 2224 df-clel 2227 df-nfc 2363 df-ral 2515 df-rex 2516 df-v 2804 df-sbc 3032 df-un 3204 df-in 3206 df-ss 3213 df-pw 3654 df-sn 3675 df-pr 3676 df-op 3678 df-uni 3894 df-br 4089 df-opab 4151 df-mpt 4152 df-id 4390 df-xp 4731 df-rel 4732 df-cnv 4733 df-co 4734 df-dm 4735 df-rn 4736 df-iota 5286 df-fun 5328 df-fn 5329 df-f 5330 df-fo 5332 df-fv 5334 df-1st 6302

This theorem is referenced by: elxp7 6332 xpopth 6338 eqop 6339 2nd1st 6342 2ndrn 6345 releldm2 6347 reldm 6348 dfoprab3 6353 elopabi 6359 mpofvex 6369 dfmpo 6387 cnvf1olem 6388 cnvoprab 6398 f1od2 6399 disjxp1 6400 elmpom 6402 xpmapenlem 7034 cnref1o 9884 fsumcnv 11997 fprodcnv 12185 qredeu 12668 qnumval 12756 xpsff1o 13431 txbas 14981 txdis 15000 vtxvalg 15866 vtxex 15868 wlkelvv 16199 wlk2f 16201