Theorem snex 4230

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	|- A e. _V

Assertion

Ref	Expression
snex	|- { A } e. _V

Proof of Theorem snex

Step	Hyp	Ref	Expression
1		snex.1	. 2 |- A e. _V
2		snexg 4229	. 2 |- ( A e. _V -> { A } e. _V )
3	1, 2	ax-mp 5	1 |- { A } e. _V

Syntax hints:   e. wcel 2176   _Vcvv 2772   {csn 3633

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639

This theorem is referenced by:  snelpw  4258  rext  4260  sspwb  4261  intid  4269  euabex  4270  mss  4271  exss  4272  opi1  4277  opeqsn  4298  opeqpr  4299  uniop  4301  snnex  4496  op1stb  4526  dtruex  4608  relop  4829  funopg  5306  funopsn  5764  fo1st  6245  fo2nd  6246  mapsn  6779  mapsnconst  6783  mapsncnv  6784  mapsnf1o2  6785  elixpsn  6824  ixpsnf1o  6825  ensn1  6890  mapsnen  6905  xpsnen  6918  endisj  6921  xpcomco  6923  xpassen  6927  phplem2  6952  findcard2  6988  findcard2s  6989  ac6sfi  6997  xpfi  7031  djuex  7147  0ct  7211  finomni  7244  exmidfodomrlemim  7311  djuassen  7331  cc2lem  7380  nn0ex  9303  xnn0nnen  10584  fxnn0nninf  10586  inftonninf  10589  hashxp  10973  nninfct  12395  fngsum  13253  znval  14431  fnpsr  14462  reldvg  15184  plyval  15237  elply2  15240  plyss  15243  plyco  15264  plycj  15266