Theorem vsnex 5381

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 4595	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5380	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2833	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  snexgALT  5387  rext  5403  sspwb  5404  moabex  5413  moabexOLD  5414  nnullss  5417  exss  5418  xpsspw  5766  funopg  6534  snnex  7713  soex  7873  opabex3d  7919  opabex3rd  7920  opabex3  7921  fo1st  7963  fo2nd  7964  mpoexxg  8029  cnvf1o  8063  sexp2  8098  sexp3  8105  naddcllem  8614  domunsn  9067  fodomr  9068  findcard2  9101  pwfilem  9230  marypha1lem  9348  brwdom2  9490  unxpwdom2  9505  elirrvOLD  9515  epfrs  9652  dfac5lem2  10046  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem2  10074  isfin1-3  10308  hsmexlem4  10351  axcc2lem  10358  canthwe  10574  canthp1lem1  10575  uniwun  10663  rankcf  10700  hashmap  14370  hashbclem  14387  incexclem  15771  isfunc  17800  homaf  17966  symgvalstruct  19338  gsum2d2  19915  gsumcom2  19916  dprd2da  19985  mpfind  22082  pf1ind  22311  dishaus  23338  discmp  23354  dis2ndc  23416  dislly  23453  dis1stc  23455  unisngl  23483  1stckgen  23510  ptcmpfi  23769  isufil2  23864  cnextfval  24018  conway  27787  etaslts  27801  cofcutr  27932  lfuhgr1v0e  29339  gsumpart  33157  gsumwrd2dccat  33172  esum2dlem  34270  esum2d  34271  esumiun  34272  carsgclctunlem1  34495  eulerpartlemgs2  34558  bnj1452  35228  fobigcup  36114  elsingles  36132  fnsingle  36133  fvsingle  36134  dfiota3  36137  funpartlem  36158  altxpsspw  36193  exeltr  36687  bj-snsetex  37211  bj-elsngl  37216  f1omptsnlem  37591  mptsnunlem  37593  topdifinffinlem  37602  heiborlem3  38064  ispointN  40118  mzpincl  43091  mzpcompact2lem  43108  pwslnmlem1  43449  pwslnm  43451  permaxinf2lem  45368  mpct  45559  salexct3  46700  salgencntex  46701  salgensscntex  46702  sge0xp  46787  clnbgrval  48182  mpoexxg2  48698  tposideq  49247  discsntermlem  49929