Theorem vsnex 5384

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 4598	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5383	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2824	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3444  {csn 4585  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-sn 4586  df-pr 4588

This theorem is referenced by:  snexg  5385  rext  5403  sspwb  5404  moabex  5414  nnullss  5417  exss  5418  xpsspw  5763  funopg  6534  snnex  7714  soex  7877  opabex3d  7923  opabex3rd  7924  opabex3  7925  fo1st  7967  fo2nd  7968  mpoexxg  8033  cnvf1o  8067  sexp2  8102  sexp3  8109  naddcllem  8617  domunsn  9068  fodomr  9069  findcard2  9105  pwfilem  9243  marypha1lem  9360  brwdom2  9502  unxpwdom2  9517  elirrv  9525  epfrs  9660  dfac5lem2  10053  dfac5lem3  10054  dfac5lem4  10055  dfac5lem4OLD  10057  kmlem2  10081  isfin1-3  10315  hsmexlem4  10358  axcc2lem  10365  canthwe  10580  canthp1lem1  10581  uniwun  10669  rankcf  10706  hashmap  14376  hashbclem  14393  incexclem  15778  isfunc  17802  homaf  17968  symgvalstruct  19303  gsum2d2  19880  gsumcom2  19881  dprd2da  19950  mpfind  21990  pf1ind  22218  dishaus  23245  discmp  23261  dis2ndc  23323  dislly  23360  dis1stc  23362  unisngl  23390  1stckgen  23417  ptcmpfi  23676  isufil2  23771  cnextfval  23925  conway  27687  etasslt  27701  cofcutr  27808  lfuhgr1v0e  29157  gsumpart  32970  gsumwrd2dccat  32980  esum2dlem  34055  esum2d  34056  esumiun  34057  carsgclctunlem1  34281  eulerpartlemgs2  34344  bnj1452  35015  fobigcup  35861  elsingles  35879  fnsingle  35880  fvsingle  35881  dfiota3  35884  funpartlem  35903  altxpsspw  35938  bj-snsetex  36924  bj-elsngl  36929  f1omptsnlem  37297  mptsnunlem  37299  topdifinffinlem  37308  heiborlem3  37780  ispointN  39709  mzpincl  42695  mzpcompact2lem  42712  pwslnmlem1  43054  pwslnm  43056  permaxinf2lem  44975  mpct  45168  salexct3  46313  salgencntex  46314  salgensscntex  46315  sge0xp  46400  clnbgrval  47796  mpoexxg2  48299  tposideq  48849  discsntermlem  49532