Theorem snexgOLD 3909

Description: A singleton whose element exists is a set. The A ∈ 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 3910 and new proofs should use snexg 3910 instead. (Contributed by Jim Kingdon, 26-Jan-2019.) (New usage is discouraged.) TODO: remove in favor of snexg 3910.

Assertion

Ref	Expression
snexgOLD	⊢ (A ∈ V → {A} ∈ V)

Proof of Theorem snexgOLD

Step	Hyp	Ref	Expression
1		pwexg 3907	. 2 ⊢ (A ∈ V → 𝒫 A ∈ V)
2		snsspw 3509	. . 3 ⊢ {A} ⊆ 𝒫 A
3		ssexg 3870	. . 3 ⊢ (({A} ⊆ 𝒫 A ∧ 𝒫 A ∈ V) → {A} ∈ V)
4	2, 3	mpan 402	. 2 ⊢ (𝒫 A ∈ V → {A} ∈ V)
5	1, 4	syl 14	1 ⊢ (A ∈ V → {A} ∈ V)

Syntax hints:   → wi 4   ∈ wcel 1374  Vcvv 2535   ⊆ wss 2894  𝒫 cpw 3334  {csn 3350

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901

This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-v 2537  df-in 2901  df-ss 2908  df-pw 3336  df-sn 3356

This theorem is referenced by:  snelpwi  3922  snelpw  3923  rext  3925  sspwb  3926  intid  3934  euabex  3935  mss  3936  exss  3937  opexgOLD  3939  opi1  3943  opm  3945  opeqsn  3963  opeqpr  3964  uniop  3966  snnex  4131  op1stb  4159  op1stbg  4160  sucexb  4173  dtruex  4221  relop  4413  elxp4  4735  elxp5  4736  funopg  4860  1stvalg  5692  2ndvalg  5693  fo1st  5707  fo2nd  5708