Theorem snex 4317

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

Syntax hints:   ∈ wcel 2209  Vcvv 2821  {csn 3705

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4244  ax-pow 4306

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711

This theorem is referenced by:  snelpw  4347  rext  4350  sspwb  4351  intid  4359  euabex  4360  mss  4361  exss  4362  opi1  4367  opeqsn  4388  opeqpr  4389  uniop  4391  snnex  4589  op1stb  4619  dtruex  4701  relop  4925  funopg  5406  funopsn  5882  fo1st  6381  fo2nd  6382  mapsn  6962  mapsnconst  6966  mapsncnv  6967  mapsnf1o2  6968  elixpsn  7007  ixpsnf1o  7008  ensn1  7073  mapsnen  7090  dom1o  7106  xpsnen  7109  endisj  7112  xpcomco  7114  xpassen  7118  phplem2  7144  findcard2  7183  findcard2s  7184  ac6sfi  7192  xpfi  7229  mapfi  7251  djuex  7373  0ct  7437  finomni  7470  exmidfodomrlemim  7543  djuassen  7563  cc2lem  7622  nn0ex  9548  xnn0nnen  10852  fxnn0nninf  10854  inftonninf  10857  hashxp  11245  hashf1lem1  11263  nninfct  12796  fngzsum  13685  znval  14943  fnpsr  14974  reldvg  15703  plyval  15756  elply2  15759  plyss  15762  plyco  15783  plycj  15785