Theorem snex 4026

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

Syntax hints:   ∈ wcel 1439  Vcvv 2620  {csn 3450

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-pow 4015

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-v 2622  df-in 3006  df-ss 3013  df-pw 3435  df-sn 3456

This theorem is referenced by:  snelpw  4049  rext  4051  sspwb  4052  intid  4060  euabex  4061  mss  4062  exss  4063  opi1  4068  opeqsn  4088  opeqpr  4089  uniop  4091  snnex  4283  op1stb  4313  dtruex  4388  relop  4599  funopg  5061  fo1st  5942  fo2nd  5943  mapsn  6461  mapsnconst  6465  mapsncnv  6466  mapsnf1o2  6467  elixpsn  6506  ixpsnf1o  6507  ensn1  6567  mapsnen  6582  xpsnen  6591  endisj  6594  xpcomco  6596  xpassen  6600  phplem2  6623  findcard2  6659  findcard2s  6660  ac6sfi  6668  xpfi  6694  djuex  6790  0ct  6843  finomni  6857  exmidfodomrlemim  6888  nn0ex  8740  fxnn0nninf  9905  inftonninf  9908  hashxp  10295