1stexg - Intuitionistic Logic Explorer

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

Theorem 1stexg 6319

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 2811	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		fo1st 6309	. . . 4 ⊢ 1^st :V–onto→V
3		fofn 5552	. . . 4 ⊢ (1^st :V–onto→V → 1^st Fn V)
4	2, 3	ax-mp 5	. . 3 ⊢ 1^st Fn V
5		funfvex 5646	. . . 4 ⊢ ((Fun 1^st ∧ 𝐴 ∈ dom 1^st ) → (1^st ‘𝐴) ∈ V)
6	5	funfni 5423	. . 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 2200 Vcvv 2799 Fn wfn 5313 –onto→wfo 5316 ‘cfv 5318 1^st c1st 6290

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 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-sep 4202 ax-pow 4258 ax-pr 4293 ax-un 4524

This theorem depends on definitions: df-bi 117 df-3an 1004 df-tru 1398 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ral 2513 df-rex 2514 df-v 2801 df-sbc 3029 df-un 3201 df-in 3203 df-ss 3210 df-pw 3651 df-sn 3672 df-pr 3673 df-op 3675 df-uni 3889 df-br 4084 df-opab 4146 df-mpt 4147 df-id 4384 df-xp 4725 df-rel 4726 df-cnv 4727 df-co 4728 df-dm 4729 df-rn 4730 df-iota 5278 df-fun 5320 df-fn 5321 df-f 5322 df-fo 5324 df-fv 5326 df-1st 6292

This theorem is referenced by: elxp7 6322 xpopth 6328 eqop 6329 2nd1st 6332 2ndrn 6335 releldm2 6337 reldm 6338 dfoprab3 6343 elopabi 6347 mpofvex 6357 dfmpo 6375 cnvf1olem 6376 cnvoprab 6386 f1od2 6387 disjxp1 6388 xpmapenlem 7018 cnref1o 9858 fsumcnv 11963 fprodcnv 12151 qredeu 12634 qnumval 12722 xpsff1o 13397 txbas 14947 txdis 14966 vtxvalg 15832 vtxex 15834 wlkelvv 16090 wlk2f 16092