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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  {csn 4583  {cpr 4585

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 5390

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 4151  df-sn 4584  df-pr 4586

This theorem is used by:  snexgALT  5398  rext  5415  sspwb  5416  moabex  5425  moabexOLD  5426  nnullss  5429  exss  5430  xpsspw  5786  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  8686  domunsn  9147  fodomr  9148  findcard2  9181  pwfilem  9310  marypha1lem  9426  brwdom2  9568  unxpwdom2  9583  elirrvOLDOLD  9594  epfrs  9733  dfac5lem2  10204  dfac5lem3  10205  dfac5lem4  10206  kmlem2  10231  isfin1-3  10465  hsmexlem4  10508  axcc2lem  10515  canthwe  10737  canthp1lem1  10738  uniwun  10826  rankcf  10863  hashmap  14581  hashbclem  14598  incexclem  16006  isfunc  18040  homaf  18206  symgvalstruct  19612  gsum2d2  20189  gsumcom2  20190  dprd2da  20259  mpfind  22425  pf1ind  22674  dishaus  23701  discmp  23717  dis2ndc  23780  dislly  23817  dis1stc  23819  unisngl  23847  1stckgen  23874  ptcmpfi  24133  isufil2  24228  cnextfval  24382  conway  28166  etaslts  28180  cofcutr  28311  istrkg2ld  28923  lfuhgr1v0e  29836  gsumpart  33667  gsumwrd2dccat  33682  esum2dlem  34767  esum2d  34768  esumiun  34769  carsgclctunlem1  34992  eulerpartlemgs2  35055  bnj1452  35725  fobigcup  36705  elsingles  36723  fnsingle  36724  fvsingle  36725  dfiota3  36728  funpartlem  36749  altxpsspw  36785  axtco  37302  ttcid  37323  ttcmin  37327  dfttc4lem2  37360  mh-inf3sn  37373  mh-infprim2bi  37378  bj-snsetex  37919  bj-elsngl  37924  f1omptsnlem  38303  mptsnunlem  38305  topdifinffinlem  38314  negprop  38687  heiborlem3  38791  ispointN  40843  mzpincl  43789  mzpcompact2lem  43806  pwslnmlem1  44138  pwslnm  44140  permaxinf2lem  46046  mpct  46259  salexct3  47396  salgencntex  47397  salgensscntex  47398  sge0xp  47483  clnbgrval  48964  mpoexxg2  49494  tposideq  50040  discsntermlem  50722