Theorem snex 4298

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

Syntax hints:   ∈ wcel 2203  Vcvv 2813  {csn 3689

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695

This theorem is referenced by:  snelpw  4328  rext  4331  sspwb  4332  intid  4340  euabex  4341  mss  4342  exss  4343  opi1  4348  opeqsn  4369  opeqpr  4370  uniop  4372  snnex  4569  op1stb  4599  dtruex  4681  relop  4905  funopg  5386  funopsn  5860  fo1st  6351  fo2nd  6352  mapsn  6925  mapsnconst  6929  mapsncnv  6930  mapsnf1o2  6931  elixpsn  6970  ixpsnf1o  6971  ensn1  7036  mapsnen  7053  dom1o  7069  xpsnen  7072  endisj  7075  xpcomco  7077  xpassen  7081  phplem2  7107  findcard2  7146  findcard2s  7147  ac6sfi  7155  xpfi  7192  mapfi  7214  djuex  7334  0ct  7398  finomni  7431  exmidfodomrlemim  7504  djuassen  7524  cc2lem  7580  nn0ex  9502  xnn0nnen  10799  fxnn0nninf  10801  inftonninf  10804  hashxp  11191  nninfct  12737  fngsum  13601  znval  14784  fnpsr  14815  reldvg  15544  plyval  15597  elply2  15600  plyss  15603  plyco  15624  plycj  15626