Theorem vsnex 5373

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 5372	. 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 5232  ax-pr 5371

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  5379  rext  5396  sspwb  5397  moabex  5406  moabexOLD  5407  nnullss  5410  exss  5411  xpsspw  5759  funopg  6527  snnex  7706  soex  7866  opabex3d  7912  opabex3rd  7913  opabex3  7914  fo1st  7956  fo2nd  7957  mpoexxg  8022  cnvf1o  8055  sexp2  8090  sexp3  8097  naddcllem  8606  domunsn  9059  fodomr  9060  findcard2  9093  pwfilem  9222  marypha1lem  9340  brwdom2  9482  unxpwdom2  9497  elirrvOLD  9507  epfrs  9646  dfac5lem2  10040  dfac5lem3  10041  dfac5lem4  10042  dfac5lem4OLD  10044  kmlem2  10068  isfin1-3  10302  hsmexlem4  10345  axcc2lem  10352  canthwe  10568  canthp1lem1  10569  uniwun  10657  rankcf  10694  hashmap  14391  hashbclem  14408  incexclem  15795  isfunc  17825  homaf  17991  symgvalstruct  19366  gsum2d2  19943  gsumcom2  19944  dprd2da  20013  mpfind  22106  pf1ind  22333  dishaus  23360  discmp  23376  dis2ndc  23438  dislly  23475  dis1stc  23477  unisngl  23505  1stckgen  23532  ptcmpfi  23791  isufil2  23886  cnextfval  24040  conway  27788  etaslts  27802  cofcutr  27933  istrkg2ld  28545  lfuhgr1v0e  29340  gsumpart  33142  gsumwrd2dccat  33157  esum2dlem  34255  esum2d  34256  esumiun  34257  carsgclctunlem1  34480  eulerpartlemgs2  34543  bnj1452  35213  fobigcup  36099  elsingles  36117  fnsingle  36118  fvsingle  36119  dfiota3  36122  funpartlem  36143  altxpsspw  36178  axtco  36672  ttcid  36693  ttcmin  36697  dfttc4lem2  36730  mh-inf3sn  36743  mh-infprim2bi  36748  bj-snsetex  37289  bj-elsngl  37294  f1omptsnlem  37669  mptsnunlem  37671  topdifinffinlem  37680  heiborlem3  38151  ispointN  40205  mzpincl  43183  mzpcompact2lem  43200  pwslnmlem1  43541  pwslnm  43543  permaxinf2lem  45460  mpct  45651  salexct3  46791  salgencntex  46792  salgensscntex  46793  sge0xp  46878  clnbgrval  48313  mpoexxg2  48829  tposideq  49378  discsntermlem  50060