Theorem vsnex 5408

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 4604	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5407	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2861	1 ⊢ {𝑥} ∈ V

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  {csn 4591  {cpr 4593

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  snexgALT  5414  rext  5431  sspwb  5432  moabex  5441  moabexOLD  5442  nnullss  5445  exss  5446  xpsspw  5798  funopg  6574  snnex  7763  soex  7924  opabex3d  7968  opabex3rd  7969  opabex3  7970  fo1st  8012  fo2nd  8013  mpoexxg  8078  cnvf1o  8112  sexp2  8148  sexp3  8155  naddcllem  8668  domunsn  9122  fodomr  9123  findcard2  9156  pwfilem  9284  marypha1lem  9400  brwdom2  9542  unxpwdom2  9557  elirrvOLDOLD  9568  epfrs  9707  dfac5lem2  10124  dfac5lem3  10125  dfac5lem4  10126  kmlem2  10151  isfin1-3  10385  hsmexlem4  10428  axcc2lem  10435  canthwe  10653  canthp1lem1  10654  uniwun  10742  rankcf  10779  hashmap  14492  hashbclem  14509  incexclem  15915  isfunc  17945  homaf  18111  symgvalstruct  19513  gsum2d2  20090  gsumcom2  20091  dprd2da  20160  mpfind  22318  pf1ind  22567  dishaus  23591  discmp  23607  dis2ndc  23670  dislly  23707  dis1stc  23709  unisngl  23737  1stckgen  23764  ptcmpfi  24023  isufil2  24118  cnextfval  24272  conway  28025  etaslts  28039  cofcutr  28170  istrkg2ld  28782  lfuhgr1v0e  29664  gsumpart  33449  gsumwrd2dccat  33464  esum2dlem  34548  esum2d  34549  esumiun  34550  carsgclctunlem1  34774  eulerpartlemgs2  34837  bnj1452  35507  fobigcup  36429  elsingles  36447  fnsingle  36448  fvsingle  36449  dfiota3  36452  funpartlem  36473  altxpsspw  36508  axtco  37041  ttcid  37062  ttcmin  37066  dfttc4lem2  37099  mh-inf3sn  37112  mh-infprim2bi  37117  bj-snsetex  37658  bj-elsngl  37663  f1omptsnlem  38041  mptsnunlem  38043  topdifinffinlem  38052  heiborlem3  38524  ispointN  40576  mzpincl  43525  mzpcompact2lem  43542  pwslnmlem1  43879  pwslnm  43881  permaxinf2lem  45781  mpct  45978  salexct3  47116  salgencntex  47117  salgensscntex  47118  sge0xp  47203  clnbgrval  48647  mpoexxg2  49177  tposideq  49725  discsntermlem  50407