Theorem vsnex 5364

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 4568	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5363	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2835	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2119  Vcvv 3431  {csn 4555  {cpr 4557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-sn 4556  df-pr 4558

This theorem is referenced by:  snexgALT  5370  rext  5387  sspwb  5388  moabex  5397  moabexOLD  5398  nnullss  5401  exss  5402  xpsspw  5752  funopg  6519  snnex  7701  soex  7861  opabex3d  7907  opabex3rd  7908  opabex3  7909  fo1st  7951  fo2nd  7952  mpoexxg  8017  cnvf1o  8050  sexp2  8086  sexp3  8093  naddcllem  8602  domunsn  9055  fodomr  9056  findcard2  9089  pwfilem  9218  marypha1lem  9336  brwdom2  9478  unxpwdom2  9493  elirrvOLDOLD  9504  epfrs  9643  dfac5lem2  10037  dfac5lem3  10038  dfac5lem4  10039  dfac5lem4OLD  10041  kmlem2  10065  isfin1-3  10299  hsmexlem4  10342  axcc2lem  10349  canthwe  10565  canthp1lem1  10566  uniwun  10654  rankcf  10691  hashmap  14388  hashbclem  14405  incexclem  15792  isfunc  17822  homaf  17988  symgvalstruct  19363  gsum2d2  19940  gsumcom2  19941  dprd2da  20010  mpfind  22091  pf1ind  22341  dishaus  23365  discmp  23381  dis2ndc  23443  dislly  23480  dis1stc  23482  unisngl  23510  1stckgen  23537  ptcmpfi  23796  isufil2  23891  cnextfval  24045  conway  27789  etaslts  27803  cofcutr  27934  istrkg2ld  28546  lfuhgr1v0e  29341  gsumpart  33144  gsumwrd2dccat  33159  esum2dlem  34276  esum2d  34277  esumiun  34278  carsgclctunlem1  34501  eulerpartlemgs2  34564  bnj1452  35234  fobigcup  36126  elsingles  36144  fnsingle  36145  fvsingle  36146  dfiota3  36149  funpartlem  36170  altxpsspw  36205  axtco  36699  ttcid  36720  ttcmin  36724  dfttc4lem2  36757  mh-inf3sn  36770  mh-infprim2bi  36775  bj-snsetex  37316  bj-elsngl  37321  f1omptsnlem  37698  mptsnunlem  37700  topdifinffinlem  37709  heiborlem3  38180  ispointN  40234  mzpincl  43183  mzpcompact2lem  43200  pwslnmlem1  43537  pwslnm  43539  permaxinf2lem  45456  mpct  45647  salexct3  46785  salgencntex  46786  salgensscntex  46787  sge0xp  46872  clnbgrval  48313  mpoexxg2  48829  tposideq  49378  discsntermlem  50060