ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  snexgOLD GIF version

Theorem snexgOLD 3960
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. This is a special case of snexg 3961 and new proofs should use snexg 3961 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) (Proof modification is discouraged.) TODO: replace its uses by uses of snexg 3961 and then remove it.
Assertion
Ref Expression
snexgOLD (𝐴 ∈ V → {𝐴} ∈ V)

Proof of Theorem snexgOLD
StepHypRef Expression
1 pwexg 3958 . 2 (𝐴 ∈ V → 𝒫 𝐴 ∈ V)
2 snsspw 3560 . . 3 {𝐴} ⊆ 𝒫 𝐴
3 ssexg 3921 . . 3 (({𝐴} ⊆ 𝒫 𝐴 ∧ 𝒫 𝐴 ∈ V) → {𝐴} ∈ V)
42, 3mpan 408 . 2 (𝒫 𝐴 ∈ V → {𝐴} ∈ V)
51, 4syl 14 1 (𝐴 ∈ V → {𝐴} ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1407  Vcvv 2572  wss 2942  𝒫 cpw 3384  {csn 3400
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-sep 3900  ax-pow 3952
This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-v 2574  df-in 2949  df-ss 2956  df-pw 3386  df-sn 3406
This theorem is referenced by:  snelpwi  3973  snelpw  3974  rext  3976  sspwb  3977  intid  3985  euabex  3986  mss  3987  exss  3988  opexgOLD  3990  opi1  3994  opm  3996  opeqsn  4014  opeqpr  4015  uniop  4017  snnex  4206  op1stb  4234  op1stbg  4235  sucexb  4248  dtruex  4308  relop  4511  elxp4  4833  elxp5  4834  funopg  4959  1stvalg  5794  2ndvalg  5795  fo1st  5809  fo2nd  5810
  Copyright terms: Public domain W3C validator