Theorem snex 4237

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

Syntax hints:   ∈ wcel 2177  Vcvv 2773  {csn 3638

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644

This theorem is referenced by:  snelpw  4265  rext  4267  sspwb  4268  intid  4276  euabex  4277  mss  4278  exss  4279  opi1  4284  opeqsn  4305  opeqpr  4306  uniop  4308  snnex  4503  op1stb  4533  dtruex  4615  relop  4836  funopg  5314  funopsn  5775  fo1st  6256  fo2nd  6257  mapsn  6790  mapsnconst  6794  mapsncnv  6795  mapsnf1o2  6796  elixpsn  6835  ixpsnf1o  6836  ensn1  6901  mapsnen  6917  xpsnen  6931  endisj  6934  xpcomco  6936  xpassen  6940  phplem2  6965  findcard2  7001  findcard2s  7002  ac6sfi  7010  xpfi  7044  djuex  7160  0ct  7224  finomni  7257  exmidfodomrlemim  7325  djuassen  7345  cc2lem  7398  nn0ex  9321  xnn0nnen  10604  fxnn0nninf  10606  inftonninf  10609  hashxp  10993  nninfct  12437  fngsum  13295  znval  14473  fnpsr  14504  reldvg  15226  plyval  15279  elply2  15282  plyss  15285  plyco  15306  plycj  15308  dom1o  16067