Theorem vsnex 5373

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 4590	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5372	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2824	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3436  {csn 4577  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-sn 4578  df-pr 4580

This theorem is referenced by:  snexg  5374  rext  5391  sspwb  5392  moabex  5402  nnullss  5405  exss  5406  xpsspw  5752  funopg  6516  snnex  7694  soex  7854  opabex3d  7900  opabex3rd  7901  opabex3  7902  fo1st  7944  fo2nd  7945  mpoexxg  8010  cnvf1o  8044  sexp2  8079  sexp3  8086  naddcllem  8594  domunsn  9044  fodomr  9045  findcard2  9078  pwfilem  9207  marypha1lem  9323  brwdom2  9465  unxpwdom2  9480  elirrvOLD  9490  epfrs  9627  dfac5lem2  10018  dfac5lem3  10019  dfac5lem4  10020  dfac5lem4OLD  10022  kmlem2  10046  isfin1-3  10280  hsmexlem4  10323  axcc2lem  10330  canthwe  10545  canthp1lem1  10546  uniwun  10634  rankcf  10671  hashmap  14342  hashbclem  14359  incexclem  15743  isfunc  17771  homaf  17937  symgvalstruct  19276  gsum2d2  19853  gsumcom2  19854  dprd2da  19923  mpfind  22012  pf1ind  22240  dishaus  23267  discmp  23283  dis2ndc  23345  dislly  23382  dis1stc  23384  unisngl  23412  1stckgen  23439  ptcmpfi  23698  isufil2  23793  cnextfval  23947  conway  27710  etasslt  27724  cofcutr  27837  lfuhgr1v0e  29199  gsumpart  33010  gsumwrd2dccat  33020  esum2dlem  34059  esum2d  34060  esumiun  34061  carsgclctunlem1  34285  eulerpartlemgs2  34348  bnj1452  35019  fobigcup  35878  elsingles  35896  fnsingle  35897  fvsingle  35898  dfiota3  35901  funpartlem  35920  altxpsspw  35955  bj-snsetex  36941  bj-elsngl  36946  f1omptsnlem  37314  mptsnunlem  37316  topdifinffinlem  37325  heiborlem3  37797  ispointN  39725  mzpincl  42711  mzpcompact2lem  42728  pwslnmlem1  43069  pwslnm  43071  permaxinf2lem  44990  mpct  45183  salexct3  46327  salgencntex  46328  salgensscntex  46329  sge0xp  46414  clnbgrval  47810  mpoexxg2  48326  tposideq  48876  discsntermlem  49559