Theorem vsnex 5440

Description: A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.)

Assertion

Ref	Expression
vsnex	⊢ {𝑥} ∈ V

Proof of Theorem vsnex

Step	Hyp	Ref	Expression
1		dfsn2 4644	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5439	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2835	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3478  {csn 4631  {cpr 4633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  snexg  5441  rext  5459  sspwb  5460  moabex  5470  nnullss  5473  exss  5474  xpsspw  5822  funopg  6602  snnex  7777  soex  7944  opabex3d  7989  opabex3rd  7990  opabex3  7991  fo1st  8033  fo2nd  8034  mpoexxg  8099  cnvf1o  8135  sexp2  8170  sexp3  8177  naddcllem  8713  domunsn  9166  fodomr  9167  findcard2  9203  pwfilem  9354  marypha1lem  9471  brwdom2  9611  unxpwdom2  9626  elirrv  9634  epfrs  9769  dfac5lem2  10162  dfac5lem3  10163  dfac5lem4  10164  dfac5lem4OLD  10166  kmlem2  10190  isfin1-3  10424  hsmexlem4  10467  axcc2lem  10474  canthwe  10689  canthp1lem1  10690  uniwun  10778  rankcf  10815  hashmap  14471  hashbclem  14488  incexclem  15869  isfunc  17915  homaf  18084  symgvalstruct  19429  gsum2d2  20007  gsumcom2  20008  dprd2da  20077  mpfind  22149  pf1ind  22375  dishaus  23406  discmp  23422  dis2ndc  23484  dislly  23521  dis1stc  23523  unisngl  23551  1stckgen  23578  ptcmpfi  23837  isufil2  23932  cnextfval  24086  conway  27859  etasslt  27873  cofcutr  27973  lfuhgr1v0e  29286  gsumpart  33043  gsumwrd2dccat  33053  esum2dlem  34073  esum2d  34074  esumiun  34075  carsgclctunlem1  34299  eulerpartlemgs2  34362  bnj1452  35045  fobigcup  35882  elsingles  35900  fnsingle  35901  fvsingle  35902  dfiota3  35905  funpartlem  35924  altxpsspw  35959  bj-snsetex  36946  bj-elsngl  36951  f1omptsnlem  37319  mptsnunlem  37321  topdifinffinlem  37330  heiborlem3  37800  ispointN  39725  mzpincl  42722  mzpcompact2lem  42739  pwslnmlem1  43081  pwslnm  43083  mpct  45144  salexct3  46298  salgencntex  46299  salgensscntex  46300  sge0xp  46385  clnbgrval  47747  mpoexxg2  48183