Theorem vsnex 5392

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 5391	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2858	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2142  Vcvv 3454  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-sn 4583  df-pr 4585

This theorem is referenced by:  snexgALT  5398  rext  5415  sspwb  5416  moabex  5425  moabexOLD  5426  nnullss  5429  exss  5430  xpsspw  5782  funopg  6555  snnex  7741  soex  7902  opabex3d  7946  opabex3rd  7947  opabex3  7948  fo1st  7990  fo2nd  7991  mpoexxg  8056  cnvf1o  8090  sexp2  8126  sexp3  8133  naddcllem  8646  domunsn  9099  fodomr  9100  findcard2  9133  pwfilem  9262  marypha1lem  9379  brwdom2  9521  unxpwdom2  9536  elirrvOLDOLD  9547  epfrs  9686  dfac5lem2  10080  dfac5lem3  10081  dfac5lem4  10082  dfac5lem4OLD  10084  kmlem2  10108  isfin1-3  10343  hsmexlem4  10386  axcc2lem  10393  canthwe  10609  canthp1lem1  10610  uniwun  10698  rankcf  10735  hashmap  14448  hashbclem  14465  incexclem  15866  isfunc  17897  homaf  18063  symgvalstruct  19437  gsum2d2  20014  gsumcom2  20015  dprd2da  20084  mpfind  22168  pf1ind  22418  dishaus  23442  discmp  23458  dis2ndc  23520  dislly  23557  dis1stc  23559  unisngl  23587  1stckgen  23614  ptcmpfi  23873  isufil2  23968  cnextfval  24122  conway  27872  etaslts  27886  cofcutr  28017  istrkg2ld  28629  lfuhgr1v0e  29455  gsumpart  33243  gsumwrd2dccat  33258  esum2dlem  34389  esum2d  34390  esumiun  34391  carsgclctunlem1  34614  eulerpartlemgs2  34677  bnj1452  35347  fobigcup  36248  elsingles  36266  fnsingle  36267  fvsingle  36268  dfiota3  36271  funpartlem  36292  altxpsspw  36327  axtco  36831  ttcid  36852  ttcmin  36856  dfttc4lem2  36889  mh-inf3sn  36902  mh-infprim2bi  36907  bj-snsetex  37448  bj-elsngl  37453  f1omptsnlem  37830  mptsnunlem  37832  topdifinffinlem  37841  heiborlem3  38312  ispointN  40366  mzpincl  43315  mzpcompact2lem  43332  pwslnmlem1  43669  pwslnm  43671  permaxinf2lem  45588  mpct  45778  salexct3  46916  salgencntex  46917  salgensscntex  46918  sge0xp  47003  clnbgrval  48444  mpoexxg2  48960  tposideq  49509  discsntermlem  50191