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  17806  homaf  17972  symgvalstruct  19311  gsum2d2  19888  gsumcom2  19889  dprd2da  19958  mpfind  22047  pf1ind  22275  dishaus  23302  discmp  23318  dis2ndc  23380  dislly  23417  dis1stc  23419  unisngl  23447  1stckgen  23474  ptcmpfi  23733  isufil2  23828  cnextfval  23982  conway  27745  etasslt  27759  cofcutr  27872  lfuhgr1v0e  29234  gsumpart  33040  gsumwrd2dccat  33050  esum2dlem  34075  esum2d  34076  esumiun  34077  carsgclctunlem1  34301  eulerpartlemgs2  34364  bnj1452  35035  fobigcup  35881  elsingles  35899  fnsingle  35900  fvsingle  35901  dfiota3  35904  funpartlem  35923  altxpsspw  35958  bj-snsetex  36944  bj-elsngl  36949  f1omptsnlem  37317  mptsnunlem  37319  topdifinffinlem  37328  heiborlem3  37800  ispointN  39729  mzpincl  42715  mzpcompact2lem  42732  pwslnmlem1  43074  pwslnm  43076  permaxinf2lem  44995  mpct  45188  salexct3  46333  salgencntex  46334  salgensscntex  46335  sge0xp  46420  clnbgrval  47816  mpoexxg2  48319  tposideq  48869  discsntermlem  49552