Theorem vsnex 5393

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 4597	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5392	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2857	1 ⊢ {𝑥} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  snexgALT  5399  rext  5416  sspwb  5417  moabex  5426  moabexOLD  5427  nnullss  5430  exss  5431  xpsspw  5787  funopg  6574  snnex  7772  soex  7933  opabex3d  7977  opabex3rd  7978  opabex3  7979  fo1st  8021  fo2nd  8022  mpoexxg  8088  cnvf1o  8122  sexp2  8163  sexp3  8170  naddcllem  8685  domunsn  9146  fodomr  9147  findcard2  9180  pwfilem  9309  marypha1lem  9425  brwdom2  9567  unxpwdom2  9582  elirrvOLDOLD  9593  epfrs  9732  dfac5lem2  10203  dfac5lem3  10204  dfac5lem4  10205  kmlem2  10230  isfin1-3  10464  hsmexlem4  10507  axcc2lem  10514  canthwe  10736  canthp1lem1  10737  uniwun  10825  rankcf  10862  hashmap  14580  hashbclem  14597  incexclem  16005  isfunc  18039  homaf  18205  symgvalstruct  19611  gsum2d2  20188  gsumcom2  20189  dprd2da  20258  mpfind  22424  pf1ind  22673  dishaus  23700  discmp  23716  dis2ndc  23779  dislly  23816  dis1stc  23818  unisngl  23846  1stckgen  23873  ptcmpfi  24132  isufil2  24227  cnextfval  24381  conway  28165  etaslts  28179  cofcutr  28310  istrkg2ld  28922  lfuhgr1v0e  29835  gsumpart  33624  gsumwrd2dccat  33639  esum2dlem  34724  esum2d  34725  esumiun  34726  carsgclctunlem1  34949  eulerpartlemgs2  35012  bnj1452  35682  fobigcup  36662  elsingles  36680  fnsingle  36681  fvsingle  36682  dfiota3  36685  funpartlem  36706  altxpsspw  36742  axtco  37259  ttcid  37280  ttcmin  37284  dfttc4lem2  37317  mh-inf3sn  37330  mh-infprim2bi  37335  bj-snsetex  37876  bj-elsngl  37881  f1omptsnlem  38259  mptsnunlem  38261  topdifinffinlem  38270  negprop  38643  heiborlem3  38747  ispointN  40799  mzpincl  43744  mzpcompact2lem  43761  pwslnmlem1  44093  pwslnm  44095  permaxinf2lem  46001  mpct  46214  salexct3  47351  salgencntex  47352  salgensscntex  47353  sge0xp  47438  clnbgrval  48919  mpoexxg2  49449  tposideq  49995  discsntermlem  50677