Theorem snex 4169

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

Syntax hints:   e. wcel 2141   _Vcvv 2730   {csn 3581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587

This theorem is referenced by:  snelpw  4196  rext  4198  sspwb  4199  intid  4207  euabex  4208  mss  4209  exss  4210  opi1  4215  opeqsn  4235  opeqpr  4236  uniop  4238  snnex  4431  op1stb  4461  dtruex  4541  relop  4759  funopg  5230  fo1st  6133  fo2nd  6134  mapsn  6664  mapsnconst  6668  mapsncnv  6669  mapsnf1o2  6670  elixpsn  6709  ixpsnf1o  6710  ensn1  6770  mapsnen  6785  xpsnen  6795  endisj  6798  xpcomco  6800  xpassen  6804  phplem2  6827  findcard2  6863  findcard2s  6864  ac6sfi  6872  xpfi  6903  djuex  7016  0ct  7080  finomni  7112  exmidfodomrlemim  7165  djuassen  7181  cc2lem  7215  nn0ex  9128  fxnn0nninf  10381  inftonninf  10384  hashxp  10748  reldvg  13401