![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > snexg | GIF version |
Description: A singleton whose element exists is a set. The 𝐴 ∈ V case of Theorem 7.12 of [Quine] p. 51, proved using only Extensionality, Power Set, and Separation. Replacement is not needed. (Contributed by Jim Kingdon, 1-Sep-2018.) |
Ref | Expression |
---|---|
snexg | ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwexg 4198 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | |
2 | snsspw 3779 | . . 3 ⊢ {𝐴} ⊆ 𝒫 𝐴 | |
3 | ssexg 4157 | . . 3 ⊢ (({𝐴} ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V) → {𝐴} ∈ V) | |
4 | 2, 3 | mpan 424 | . 2 ⊢ (𝒫 𝐴 ∈ V → {𝐴} ∈ V) |
5 | 1, 4 | syl 14 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 Vcvv 2752 ⊆ wss 3144 𝒫 cpw 3590 {csn 3607 |
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 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4192 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 |
This theorem is referenced by: snex 4203 notnotsnex 4205 exmidsssnc 4221 snelpwi 4230 opexg 4246 opm 4252 tpexg 4462 op1stbg 4497 sucexb 4514 elxp4 5134 elxp5 5135 opabex3d 6146 opabex3 6147 1stvalg 6167 2ndvalg 6168 mpoexxg 6235 cnvf1o 6250 brtpos2 6276 tfr0dm 6347 tfrlemisucaccv 6350 tfrlemibxssdm 6352 tfrlemibfn 6353 tfr1onlemsucaccv 6366 tfr1onlembxssdm 6368 tfr1onlembfn 6369 tfrcllemsucaccv 6379 tfrcllembxssdm 6381 tfrcllembfn 6382 fvdiagfn 6719 ixpsnf1o 6762 mapsnf1o 6763 xpsnen2g 6855 zfz1isolem1 10852 climconst2 11331 ennnfonelemp1 12457 setsvalg 12542 setsex 12544 setsslid 12563 strle1g 12618 1strbas 12629 imasex 12782 imasival 12783 imasbas 12784 imasplusg 12785 imasmulr 12786 mgm1 12846 sgrp1 12874 mnd1 12907 mnd1id 12908 grp1 13050 grp1inv 13051 triv1nsgd 13157 ring1 13411 znval 13932 znle 13933 znbaslemnn 13935 znbas 13939 psrval 13944 psrbasg 13951 |
Copyright terms: Public domain | W3C validator |