Theorem vsnex 5407

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 4607	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5406	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2865	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2149  Vcvv 3463  {csn 4594  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  snexgALT  5413  rext  5430  sspwb  5431  moabex  5440  moabexOLD  5441  nnullss  5444  exss  5445  xpsspw  5797  funopg  6571  snnex  7756  soex  7917  opabex3d  7961  opabex3rd  7962  opabex3  7963  fo1st  8005  fo2nd  8006  mpoexxg  8071  cnvf1o  8105  sexp2  8141  sexp3  8148  naddcllem  8661  domunsn  9114  fodomr  9115  findcard2  9148  pwfilem  9276  marypha1lem  9392  brwdom2  9534  unxpwdom2  9549  elirrvOLDOLD  9560  epfrs  9699  dfac5lem2  10107  dfac5lem3  10108  dfac5lem4  10109  kmlem2  10134  isfin1-3  10369  hsmexlem4  10412  axcc2lem  10419  canthwe  10635  canthp1lem1  10636  uniwun  10724  rankcf  10761  hashmap  14471  hashbclem  14488  incexclem  15889  isfunc  17920  homaf  18086  symgvalstruct  19466  gsum2d2  20043  gsumcom2  20044  dprd2da  20113  mpfind  22234  pf1ind  22483  dishaus  23507  discmp  23523  dis2ndc  23585  dislly  23622  dis1stc  23624  unisngl  23652  1stckgen  23679  ptcmpfi  23938  isufil2  24033  cnextfval  24187  conway  27937  etaslts  27951  cofcutr  28082  istrkg2ld  28694  lfuhgr1v0e  29544  gsumpart  33323  gsumwrd2dccat  33338  esum2dlem  34426  esum2d  34427  esumiun  34428  carsgclctunlem1  34651  eulerpartlemgs2  34714  bnj1452  35384  fobigcup  36288  elsingles  36306  fnsingle  36307  fvsingle  36308  dfiota3  36311  funpartlem  36332  altxpsspw  36367  axtco  36870  ttcid  36891  ttcmin  36895  dfttc4lem2  36928  mh-inf3sn  36941  mh-infprim2bi  36946  bj-snsetex  37486  bj-elsngl  37491  f1omptsnlem  37869  mptsnunlem  37871  topdifinffinlem  37880  heiborlem3  38351  ispointN  40405  mzpincl  43356  mzpcompact2lem  43373  pwslnmlem1  43710  pwslnm  43712  permaxinf2lem  45612  mpct  45809  salexct3  46947  salgencntex  46948  salgensscntex  46949  sge0xp  47034  clnbgrval  48475  mpoexxg2  49002  tposideq  49550  discsntermlem  50232