Theorem vsnex 5372

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  {csn 4568  {cpr 4570

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 5231  ax-pr 5370

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 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  snexgALT  5378  rext  5395  sspwb  5396  moabex  5405  moabexOLD  5406  nnullss  5409  exss  5410  xpsspw  5758  funopg  6526  snnex  7705  soex  7865  opabex3d  7911  opabex3rd  7912  opabex3  7913  fo1st  7955  fo2nd  7956  mpoexxg  8021  cnvf1o  8054  sexp2  8089  sexp3  8096  naddcllem  8605  domunsn  9058  fodomr  9059  findcard2  9092  pwfilem  9221  marypha1lem  9339  brwdom2  9481  unxpwdom2  9496  elirrvOLD  9506  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  22103  pf1ind  22330  dishaus  23357  discmp  23373  dis2ndc  23435  dislly  23472  dis1stc  23474  unisngl  23502  1stckgen  23529  ptcmpfi  23788  isufil2  23883  cnextfval  24037  conway  27785  etaslts  27799  cofcutr  27930  istrkg2ld  28542  lfuhgr1v0e  29337  gsumpart  33139  gsumwrd2dccat  33154  esum2dlem  34252  esum2d  34253  esumiun  34254  carsgclctunlem1  34477  eulerpartlemgs2  34540  bnj1452  35210  fobigcup  36096  elsingles  36114  fnsingle  36115  fvsingle  36116  dfiota3  36119  funpartlem  36140  altxpsspw  36175  axtco  36669  ttcid  36690  ttcmin  36694  dfttc4lem2  36727  mh-inf3sn  36740  mh-infprim2bi  36745  bj-snsetex  37286  bj-elsngl  37291  f1omptsnlem  37666  mptsnunlem  37668  topdifinffinlem  37677  heiborlem3  38148  ispointN  40202  mzpincl  43180  mzpcompact2lem  43197  pwslnmlem1  43538  pwslnm  43540  permaxinf2lem  45457  mpct  45648  salexct3  46788  salgencntex  46789  salgensscntex  46790  sge0xp  46875  clnbgrval  48310  mpoexxg2  48826  tposideq  49375  discsntermlem  50057