Theorem snex 4228

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 4227	. 2 ⊢ (𝐴 ∈ V → {𝐴} ∈ V)
3	1, 2	ax-mp 5	1 ⊢ {𝐴} ∈ V

Syntax hints:   ∈ wcel 2175  Vcvv 2771  {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:  snelpw  4256  rext  4258  sspwb  4259  intid  4267  euabex  4268  mss  4269  exss  4270  opi1  4275  opeqsn  4295  opeqpr  4296  uniop  4298  snnex  4493  op1stb  4523  dtruex  4605  relop  4826  funopg  5302  fo1st  6233  fo2nd  6234  mapsn  6767  mapsnconst  6771  mapsncnv  6772  mapsnf1o2  6773  elixpsn  6812  ixpsnf1o  6813  ensn1  6873  mapsnen  6888  xpsnen  6898  endisj  6901  xpcomco  6903  xpassen  6907  phplem2  6932  findcard2  6968  findcard2s  6969  ac6sfi  6977  xpfi  7011  djuex  7127  0ct  7191  finomni  7224  exmidfodomrlemim  7291  djuassen  7311  cc2lem  7360  nn0ex  9283  xnn0nnen  10563  fxnn0nninf  10565  inftonninf  10568  hashxp  10952  nninfct  12281  fngsum  13138  znval  14316  fnpsr  14347  reldvg  15069  plyval  15122  elply2  15125  plyss  15128  plyco  15149  plycj  15151