| 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 4223 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | |
| 2 | snsspw 3804 | . . 3 ⊢ {𝐴} ⊆ 𝒫 𝐴 | |
| 3 | ssexg 4182 | . . 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 2175 Vcvv 2771 ⊆ wss 3165 𝒫 cpw 3615 {csn 3632 |
| 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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-14 2178 ax-ext 2186 ax-sep 4161 ax-pow 4217 |
| This theorem depends on definitions: df-bi 117 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-v 2773 df-in 3171 df-ss 3178 df-pw 3617 df-sn 3638 |
| This theorem is referenced by: snex 4228 notnotsnex 4230 exmidsssnc 4246 snelpwi 4255 opexg 4271 opm 4277 tpexg 4490 op1stbg 4525 sucexb 4544 elxp4 5169 elxp5 5170 opabex3d 6205 opabex3 6206 1stvalg 6227 2ndvalg 6228 mpoexxg 6295 cnvf1o 6310 brtpos2 6336 tfr0dm 6407 tfrlemisucaccv 6410 tfrlemibxssdm 6412 tfrlemibfn 6413 tfr1onlemsucaccv 6426 tfr1onlembxssdm 6428 tfr1onlembfn 6429 tfrcllemsucaccv 6439 tfrcllembxssdm 6441 tfrcllembfn 6442 fvdiagfn 6779 ixpsnf1o 6822 mapsnf1o 6823 xpsnen2g 6923 zfz1isolem1 10983 climconst2 11544 ennnfonelemp1 12719 setsvalg 12804 setsex 12806 setsslid 12825 strle1g 12880 1strbas 12891 pwsval 13065 pwsbas 13066 pwssnf1o 13072 imasex 13079 imasival 13080 imasbas 13081 imasplusg 13082 imasmulr 13083 mgm1 13144 igsumvalx 13163 sgrp1 13185 mnd1 13229 mnd1id 13230 grp1 13380 grp1inv 13381 mulgnngsum 13405 triv1nsgd 13496 ring1 13763 znval 14340 znle 14341 znbaslemnn 14343 znbas 14348 znzrhval 14351 znzrhfo 14352 psrval 14370 psrbasg 14378 psrplusgg 14382 |
| Copyright terms: Public domain | W3C validator |