Theorem vsnex 5377

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 4591	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5376	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2830	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2113  Vcvv 3438  {csn 4578  {cpr 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-sn 4579  df-pr 4581

This theorem is referenced by:  snexg  5378  rext  5394  sspwb  5395  moabex  5404  moabexOLD  5405  nnullss  5408  exss  5409  xpsspw  5756  funopg  6524  snnex  7701  soex  7861  opabex3d  7907  opabex3rd  7908  opabex3  7909  fo1st  7951  fo2nd  7952  mpoexxg  8017  cnvf1o  8051  sexp2  8086  sexp3  8093  naddcllem  8602  domunsn  9053  fodomr  9054  findcard2  9087  pwfilem  9216  marypha1lem  9334  brwdom2  9476  unxpwdom2  9491  elirrvOLD  9501  epfrs  9638  dfac5lem2  10032  dfac5lem3  10033  dfac5lem4  10034  dfac5lem4OLD  10036  kmlem2  10060  isfin1-3  10294  hsmexlem4  10337  axcc2lem  10344  canthwe  10560  canthp1lem1  10561  uniwun  10649  rankcf  10686  hashmap  14356  hashbclem  14373  incexclem  15757  isfunc  17786  homaf  17952  symgvalstruct  19324  gsum2d2  19901  gsumcom2  19902  dprd2da  19971  mpfind  22068  pf1ind  22297  dishaus  23324  discmp  23340  dis2ndc  23402  dislly  23439  dis1stc  23441  unisngl  23469  1stckgen  23496  ptcmpfi  23755  isufil2  23850  cnextfval  24004  conway  27767  etasslt  27781  cofcutr  27895  lfuhgr1v0e  29276  gsumpart  33095  gsumwrd2dccat  33109  esum2dlem  34198  esum2d  34199  esumiun  34200  carsgclctunlem1  34423  eulerpartlemgs2  34486  bnj1452  35157  fobigcup  36041  elsingles  36059  fnsingle  36060  fvsingle  36061  dfiota3  36064  funpartlem  36085  altxpsspw  36120  bj-snsetex  37107  bj-elsngl  37112  f1omptsnlem  37480  mptsnunlem  37482  topdifinffinlem  37491  heiborlem3  37953  ispointN  39941  mzpincl  42918  mzpcompact2lem  42935  pwslnmlem1  43276  pwslnm  43278  permaxinf2lem  45195  mpct  45387  salexct3  46528  salgencntex  46529  salgensscntex  46530  sge0xp  46615  clnbgrval  48010  mpoexxg2  48526  tposideq  49075  discsntermlem  49757