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  4296  opeqpr  4297  uniop  4299  snnex  4494  op1stb  4524  dtruex  4606  relop  4827  funopg  5304  funopsn  5761  fo1st  6242  fo2nd  6243  mapsn  6776  mapsnconst  6780  mapsncnv  6781  mapsnf1o2  6782  elixpsn  6821  ixpsnf1o  6822  ensn1  6887  mapsnen  6902  xpsnen  6915  endisj  6918  xpcomco  6920  xpassen  6924  phplem2  6949  findcard2  6985  findcard2s  6986  ac6sfi  6994  xpfi  7028  djuex  7144  0ct  7208  finomni  7241  exmidfodomrlemim  7308  djuassen  7328  cc2lem  7377  nn0ex  9300  xnn0nnen  10580  fxnn0nninf  10582  inftonninf  10585  hashxp  10969  nninfct  12304  fngsum  13162  znval  14340  fnpsr  14371  reldvg  15093  plyval  15146  elply2  15149  plyss  15152  plyco  15173  plycj  15175