1stexg - Intuitionistic Logic Explorer

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

Theorem 1stexg 6325

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 2812	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
2		fo1st 6315	. . . 4 ⊢ 1^st :V–onto→V
3		fofn 5558	. . . 4 ⊢ (1^st :V–onto→V → 1^st Fn V)
4	2, 3	ax-mp 5	. . 3 ⊢ 1^st Fn V
5		funfvex 5652	. . . 4 ⊢ ((Fun 1^st ∧ 𝐴 ∈ dom 1^st ) → (1^st ‘𝐴) ∈ V)
6	5	funfni 5429	. . 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 2800 Fn wfn 5319 –onto→wfo 5322 ‘cfv 5324 1^st c1st 6296

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 4205 ax-pow 4262 ax-pr 4297 ax-un 4528

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 2802 df-sbc 3030 df-un 3202 df-in 3204 df-ss 3211 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-br 4087 df-opab 4149 df-mpt 4150 df-id 4388 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-fo 5330 df-fv 5332 df-1st 6298

This theorem is referenced by: elxp7 6328 xpopth 6334 eqop 6335 2nd1st 6338 2ndrn 6341 releldm2 6343 reldm 6344 dfoprab3 6349 elopabi 6355 mpofvex 6365 dfmpo 6383 cnvf1olem 6384 cnvoprab 6394 f1od2 6395 disjxp1 6396 elmpom 6398 xpmapenlem 7030 cnref1o 9875 fsumcnv 11988 fprodcnv 12176 qredeu 12659 qnumval 12747 xpsff1o 13422 txbas 14972 txdis 14991 vtxvalg 15857 vtxex 15859 wlkelvv 16146 wlk2f 16148