Theorem vsnex 5409

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 4619	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5408	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2831	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3464  {csn 4606  {cpr 4608

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 2708  ax-sep 5271  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-sn 4607  df-pr 4609

This theorem is referenced by:  snexg  5410  rext  5428  sspwb  5429  moabex  5439  nnullss  5442  exss  5443  xpsspw  5793  funopg  6575  snnex  7757  soex  7922  opabex3d  7969  opabex3rd  7970  opabex3  7971  fo1st  8013  fo2nd  8014  mpoexxg  8079  cnvf1o  8115  sexp2  8150  sexp3  8157  naddcllem  8693  domunsn  9146  fodomr  9147  findcard2  9183  pwfilem  9333  marypha1lem  9450  brwdom2  9592  unxpwdom2  9607  elirrv  9615  epfrs  9750  dfac5lem2  10143  dfac5lem3  10144  dfac5lem4  10145  dfac5lem4OLD  10147  kmlem2  10171  isfin1-3  10405  hsmexlem4  10448  axcc2lem  10455  canthwe  10670  canthp1lem1  10671  uniwun  10759  rankcf  10796  hashmap  14458  hashbclem  14475  incexclem  15857  isfunc  17882  homaf  18048  symgvalstruct  19383  gsum2d2  19960  gsumcom2  19961  dprd2da  20030  mpfind  22070  pf1ind  22298  dishaus  23325  discmp  23341  dis2ndc  23403  dislly  23440  dis1stc  23442  unisngl  23470  1stckgen  23497  ptcmpfi  23756  isufil2  23851  cnextfval  24005  conway  27768  etasslt  27782  cofcutr  27889  lfuhgr1v0e  29238  gsumpart  33056  gsumwrd2dccat  33066  esum2dlem  34128  esum2d  34129  esumiun  34130  carsgclctunlem1  34354  eulerpartlemgs2  34417  bnj1452  35088  fobigcup  35923  elsingles  35941  fnsingle  35942  fvsingle  35943  dfiota3  35946  funpartlem  35965  altxpsspw  36000  bj-snsetex  36986  bj-elsngl  36991  f1omptsnlem  37359  mptsnunlem  37361  topdifinffinlem  37370  heiborlem3  37842  ispointN  39766  mzpincl  42724  mzpcompact2lem  42741  pwslnmlem1  43083  pwslnm  43085  permaxinf2lem  45004  mpct  45192  salexct3  46338  salgencntex  46339  salgensscntex  46340  sge0xp  46425  clnbgrval  47803  mpoexxg2  48280  tposideq  48830  discsntermlem  49414