Theorem vsnex 5370

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 4586	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5369	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2827	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2111  Vcvv 3436  {csn 4573  {cpr 4575

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-pr 5368

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4574  df-pr 4576

This theorem is referenced by:  snexg  5371  rext  5387  sspwb  5388  moabex  5397  nnullss  5400  exss  5401  xpsspw  5748  funopg  6515  snnex  7691  soex  7851  opabex3d  7897  opabex3rd  7898  opabex3  7899  fo1st  7941  fo2nd  7942  mpoexxg  8007  cnvf1o  8041  sexp2  8076  sexp3  8083  naddcllem  8591  domunsn  9040  fodomr  9041  findcard2  9074  pwfilem  9202  marypha1lem  9317  brwdom2  9459  unxpwdom2  9474  elirrvOLD  9484  epfrs  9621  dfac5lem2  10015  dfac5lem3  10016  dfac5lem4  10017  dfac5lem4OLD  10019  kmlem2  10043  isfin1-3  10277  hsmexlem4  10320  axcc2lem  10327  canthwe  10542  canthp1lem1  10543  uniwun  10631  rankcf  10668  hashmap  14342  hashbclem  14359  incexclem  15743  isfunc  17771  homaf  17937  symgvalstruct  19309  gsum2d2  19886  gsumcom2  19887  dprd2da  19956  mpfind  22042  pf1ind  22270  dishaus  23297  discmp  23313  dis2ndc  23375  dislly  23412  dis1stc  23414  unisngl  23442  1stckgen  23469  ptcmpfi  23728  isufil2  23823  cnextfval  23977  conway  27740  etasslt  27754  cofcutr  27868  lfuhgr1v0e  29232  gsumpart  33037  gsumwrd2dccat  33047  esum2dlem  34105  esum2d  34106  esumiun  34107  carsgclctunlem1  34330  eulerpartlemgs2  34393  bnj1452  35064  fobigcup  35942  elsingles  35960  fnsingle  35961  fvsingle  35962  dfiota3  35965  funpartlem  35986  altxpsspw  36021  bj-snsetex  37007  bj-elsngl  37012  f1omptsnlem  37380  mptsnunlem  37382  topdifinffinlem  37391  heiborlem3  37863  ispointN  39851  mzpincl  42837  mzpcompact2lem  42854  pwslnmlem1  43195  pwslnm  43197  permaxinf2lem  45115  mpct  45308  salexct3  46450  salgencntex  46451  salgensscntex  46452  sge0xp  46537  clnbgrval  47932  mpoexxg2  48448  tposideq  48998  discsntermlem  49681