![]() |
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 3980 | . 2 ⊢ (𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V) | |
2 | snsspw 3582 | . . 3 ⊢ {𝐴} ⊆ 𝒫 𝐴 | |
3 | ssexg 3943 | . . 3 ⊢ (({𝐴} ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V) → {𝐴} ∈ V) | |
4 | 2, 3 | mpan 415 | . 2 ⊢ (𝒫 𝐴 ∈ V → {𝐴} ∈ V) |
5 | 1, 4 | syl 14 | 1 ⊢ (𝐴 ∈ 𝑉 → {𝐴} ∈ V) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 Vcvv 2612 ⊆ wss 2984 𝒫 cpw 3406 {csn 3422 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3922 ax-pow 3974 |
This theorem depends on definitions: df-bi 115 df-tru 1288 df-nf 1391 df-sb 1688 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-v 2614 df-in 2990 df-ss 2997 df-pw 3408 df-sn 3428 |
This theorem is referenced by: snex 3984 notnotsnex 3986 snelpwi 4003 opexg 4019 opm 4025 tpexg 4233 op1stbg 4264 sucexb 4277 elxp4 4872 elxp5 4873 opabex3d 5827 opabex3 5828 1stvalg 5848 2ndvalg 5849 mpt2exxg 5912 cnvf1o 5925 brtpos2 5948 tfr0dm 6019 tfrlemisucaccv 6022 tfrlemibxssdm 6024 tfrlemibfn 6025 tfr1onlemsucaccv 6038 tfr1onlembxssdm 6040 tfr1onlembfn 6041 tfrcllemsucaccv 6051 tfrcllembxssdm 6053 tfrcllembfn 6054 fvdiagfn 6380 xpsnen2g 6475 climconst2 10504 |
Copyright terms: Public domain | W3C validator |