![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2ndexg | GIF version |
Description: Existence of the first member of a set. (Contributed by Jim Kingdon, 26-Jan-2019.) |
Ref | Expression |
---|---|
2ndexg | ⊢ (𝐴 ∈ 𝑉 → (2nd ‘𝐴) ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 2644 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) | |
2 | fo2nd 5967 | . . . 4 ⊢ 2nd :V–onto→V | |
3 | fofn 5270 | . . . 4 ⊢ (2nd :V–onto→V → 2nd Fn V) | |
4 | 2, 3 | ax-mp 7 | . . 3 ⊢ 2nd Fn V |
5 | funfvex 5357 | . . . 4 ⊢ ((Fun 2nd ∧ 𝐴 ∈ dom 2nd ) → (2nd ‘𝐴) ∈ V) | |
6 | 5 | funfni 5148 | . . 3 ⊢ ((2nd Fn V ∧ 𝐴 ∈ V) → (2nd ‘𝐴) ∈ V) |
7 | 4, 6 | mpan 416 | . 2 ⊢ (𝐴 ∈ V → (2nd ‘𝐴) ∈ V) |
8 | 1, 7 | syl 14 | 1 ⊢ (𝐴 ∈ 𝑉 → (2nd ‘𝐴) ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 Vcvv 2633 Fn wfn 5044 –onto→wfo 5047 ‘cfv 5049 2nd c2nd 5948 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ral 2375 df-rex 2376 df-v 2635 df-sbc 2855 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-opab 3922 df-mpt 3923 df-id 4144 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-rn 4478 df-iota 5014 df-fun 5051 df-fn 5052 df-f 5053 df-fo 5055 df-fv 5057 df-2nd 5950 |
This theorem is referenced by: elxp7 5979 xpopth 5984 eqop 5985 op1steq 5987 2nd1st 5988 2ndrn 5991 dfoprab3 5999 elopabi 6003 mpt2fvex 6011 dfmpt2 6026 cnvf1olem 6027 cnvoprab 6037 f1od2 6038 xpmapenlem 6645 djur 6837 cnref1o 9232 fsumcnv 10996 qredeu 11522 qdenval 11607 |
Copyright terms: Public domain | W3C validator |