Theorem snex 4041

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 4040	. 2 |- ( A e. _V -> { A } e. _V )
3	1, 2	ax-mp 7	1 |- { A } e. _V

Syntax hints:   e. wcel 1445   _Vcvv 2633   {csn 3466

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030

This theorem depends on definitions:  df-bi 116  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-v 2635  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472

This theorem is referenced by:  snelpw  4064  rext  4066  sspwb  4067  intid  4075  euabex  4076  mss  4077  exss  4078  opi1  4083  opeqsn  4103  opeqpr  4104  uniop  4106  snnex  4298  op1stb  4328  dtruex  4403  relop  4617  funopg  5082  fo1st  5966  fo2nd  5967  mapsn  6487  mapsnconst  6491  mapsncnv  6492  mapsnf1o2  6493  elixpsn  6532  ixpsnf1o  6533  ensn1  6593  mapsnen  6608  xpsnen  6617  endisj  6620  xpcomco  6622  xpassen  6626  phplem2  6649  findcard2  6685  findcard2s  6686  ac6sfi  6694  xpfi  6720  djuex  6816  0ct  6869  finomni  6883  exmidfodomrlemim  6924  nn0ex  8777  fxnn0nninf  9993  inftonninf  9996  hashxp  10349