Theorem vsnex 5379

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 4593	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5378	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2832	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3440  {csn 4580  {cpr 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  snexg  5380  rext  5396  sspwb  5397  moabex  5406  moabexOLD  5407  nnullss  5410  exss  5411  xpsspw  5758  funopg  6526  snnex  7703  soex  7863  opabex3d  7909  opabex3rd  7910  opabex3  7911  fo1st  7953  fo2nd  7954  mpoexxg  8019  cnvf1o  8053  sexp2  8088  sexp3  8095  naddcllem  8604  domunsn  9055  fodomr  9056  findcard2  9089  pwfilem  9218  marypha1lem  9336  brwdom2  9478  unxpwdom2  9493  elirrvOLD  9503  epfrs  9640  dfac5lem2  10034  dfac5lem3  10035  dfac5lem4  10036  dfac5lem4OLD  10038  kmlem2  10062  isfin1-3  10296  hsmexlem4  10339  axcc2lem  10346  canthwe  10562  canthp1lem1  10563  uniwun  10651  rankcf  10688  hashmap  14358  hashbclem  14375  incexclem  15759  isfunc  17788  homaf  17954  symgvalstruct  19326  gsum2d2  19903  gsumcom2  19904  dprd2da  19973  mpfind  22070  pf1ind  22299  dishaus  23326  discmp  23342  dis2ndc  23404  dislly  23441  dis1stc  23443  unisngl  23471  1stckgen  23498  ptcmpfi  23757  isufil2  23852  cnextfval  24006  conway  27775  etaslts  27789  cofcutr  27920  lfuhgr1v0e  29327  gsumpart  33146  gsumwrd2dccat  33160  esum2dlem  34249  esum2d  34250  esumiun  34251  carsgclctunlem1  34474  eulerpartlemgs2  34537  bnj1452  35208  fobigcup  36092  elsingles  36110  fnsingle  36111  fvsingle  36112  dfiota3  36115  funpartlem  36136  altxpsspw  36171  exeltr  36665  bj-snsetex  37164  bj-elsngl  37169  f1omptsnlem  37541  mptsnunlem  37543  topdifinffinlem  37552  heiborlem3  38014  ispointN  40002  mzpincl  42976  mzpcompact2lem  42993  pwslnmlem1  43334  pwslnm  43336  permaxinf2lem  45253  mpct  45445  salexct3  46586  salgencntex  46587  salgensscntex  46588  sge0xp  46673  clnbgrval  48068  mpoexxg2  48584  tposideq  49133  discsntermlem  49815