Theorem snex 4197

Description: A singleton whose element exists is a set. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.)

Hypothesis

Ref	Expression
snex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
snex	⊢ {𝐴} ∈ V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		snex.1	. 2 ⊢ 𝐴 ∈ V
2		snexg 4196	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝐴} ∈ V

Syntax hints:   ∈ wcel 2158  Vcvv 2749  {csn 3604

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610

This theorem is referenced by:  snelpw  4225  rext  4227  sspwb  4228  intid  4236  euabex  4237  mss  4238  exss  4239  opi1  4244  opeqsn  4264  opeqpr  4265  uniop  4267  snnex  4460  op1stb  4490  dtruex  4570  relop  4789  funopg  5262  fo1st  6171  fo2nd  6172  mapsn  6703  mapsnconst  6707  mapsncnv  6708  mapsnf1o2  6709  elixpsn  6748  ixpsnf1o  6749  ensn1  6809  mapsnen  6824  xpsnen  6834  endisj  6837  xpcomco  6839  xpassen  6843  phplem2  6866  findcard2  6902  findcard2s  6903  ac6sfi  6911  xpfi  6942  djuex  7055  0ct  7119  finomni  7151  exmidfodomrlemim  7213  djuassen  7229  cc2lem  7278  nn0ex  9195  fxnn0nninf  10451  inftonninf  10454  hashxp  10819  reldvg  14419