![]() |
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 4180 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | |
2 | snsspw 3764 | . . 3 ⊢ {𝐴} ⊆ 𝒫 𝐴 | |
3 | ssexg 4142 | . . 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 2148 Vcvv 2737 ⊆ wss 3129 𝒫 cpw 3575 {csn 3592 |
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 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-14 2151 ax-ext 2159 ax-sep 4121 ax-pow 4174 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2739 df-in 3135 df-ss 3142 df-pw 3577 df-sn 3598 |
This theorem is referenced by: snex 4185 notnotsnex 4187 exmidsssnc 4203 snelpwi 4212 opexg 4228 opm 4234 tpexg 4444 op1stbg 4479 sucexb 4496 elxp4 5116 elxp5 5117 opabex3d 6121 opabex3 6122 1stvalg 6142 2ndvalg 6143 mpoexxg 6210 cnvf1o 6225 brtpos2 6251 tfr0dm 6322 tfrlemisucaccv 6325 tfrlemibxssdm 6327 tfrlemibfn 6328 tfr1onlemsucaccv 6341 tfr1onlembxssdm 6343 tfr1onlembfn 6344 tfrcllemsucaccv 6354 tfrcllembxssdm 6356 tfrcllembfn 6357 fvdiagfn 6692 ixpsnf1o 6735 mapsnf1o 6736 xpsnen2g 6828 zfz1isolem1 10819 climconst2 11298 ennnfonelemp1 12406 setsvalg 12491 setsex 12493 setsslid 12512 strle1g 12564 1strbas 12575 imasex 12725 imasival 12726 imasbas 12727 imasplusg 12728 imasmulr 12729 mgm1 12788 sgrp1 12815 mnd1 12846 mnd1id 12847 grp1 12975 grp1inv 12976 triv1nsgd 13076 ring1 13234 |
Copyright terms: Public domain | W3C validator |