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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  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  5788  funopg  6579  snnex  7776  soex  7937  opabex3d  7981  opabex3rd  7982  opabex3  7983  fo1st  8025  fo2nd  8026  mpoexxg  8093  cnvf1o  8129  sexp2  8170  sexp3  8177  naddcllem  8693  domunsn  9154  fodomr  9155  findcard2  9188  pwfilem  9317  marypha1lem  9432  brwdom2  9574  unxpwdom2  9589  elirrvOLDOLD  9600  epfrs  9739  dfac5lem2  10210  dfac5lem3  10211  dfac5lem4  10212  kmlem2  10237  isfin1-3  10471  hsmexlem4  10514  axcc2lem  10521  canthwe  10743  canthp1lem1  10744  uniwun  10832  rankcf  10869  hashmap  14587  hashbclem  14604  incexclem  16014  isfunc  18048  homaf  18214  symgvalstruct  19620  gsum2d2  20197  gsumcom2  20198  dprd2da  20267  mpfind  22433  pf1ind  22682  dishaus  23709  discmp  23725  dis2ndc  23788  dislly  23825  dis1stc  23827  unisngl  23855  1stckgen  23882  ptcmpfi  24141  isufil2  24236  cnextfval  24390  conway  28174  etaslts  28188  cofcutr  28319  istrkg2ld  28931  lfuhgr1v0e  29844  gsumpart  33674  gsumwrd2dccat  33689  esum2dlem  34774  esum2d  34775  esumiun  34776  carsgclctunlem1  34999  eulerpartlemgs2  35062  bnj1452  35732  fobigcup  36786  elsingles  36804  fnsingle  36805  fvsingle  36806  dfiota3  36809  funpartlem  36830  altxpsspw  36866  axtco  37383  ttcid  37404  ttcmin  37408  dfttc4lem2  37441  mh-inf3sn  37454  mh-infprim2bi  37459  bj-snsetex  38000  bj-elsngl  38005  f1omptsnlem  38396  mptsnunlem  38398  topdifinffinlem  38407  negprop  38780  heiborlem3  38884  ispointN  40936  mzpincl  43882  mzpcompact2lem  43899  pwslnmlem1  44231  pwslnm  44233  permaxinf2lem  46138  mpct  46351  salexct3  47488  salgencntex  47489  salgensscntex  47490  sge0xp  47575  clnbgrval  49056  mpoexxg2  49586  tposideq  50137  discsntermlem  50844