Theorem vsnex 5429

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  {csn 4628  {cpr 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5299  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-sn 4629  df-pr 4631

This theorem is referenced by:  snexg  5430  rext  5448  sspwb  5449  moabex  5459  nnullss  5462  exss  5463  xpsspw  5808  funopg  6580  snnex  7742  soex  7909  opabex3d  7949  opabex3rd  7950  opabex3  7951  fo1st  7992  fo2nd  7993  mpoexxg  8059  cnvf1o  8094  sexp2  8129  sexp3  8136  naddcllem  8672  domunsn  9124  fodomr  9125  findcard2  9161  pwfilem  9174  marypha1lem  9425  brwdom2  9565  unxpwdom2  9580  elirrv  9588  epfrs  9723  dfac5lem2  10116  dfac5lem3  10117  dfac5lem4  10118  kmlem2  10143  isfin1-3  10378  hsmexlem4  10421  axcc2lem  10428  canthwe  10643  canthp1lem1  10644  uniwun  10732  rankcf  10769  hashmap  14392  hashbclem  14408  incexclem  15779  isfunc  17811  homaf  17977  symgvalstruct  19259  gsum2d2  19837  gsumcom2  19838  dprd2da  19907  mpfind  21662  pf1ind  21866  dishaus  22878  discmp  22894  dis2ndc  22956  dislly  22993  dis1stc  22995  unisngl  23023  1stckgen  23050  ptcmpfi  23309  isufil2  23404  cnextfval  23558  conway  27290  etasslt  27304  cofcutr  27401  lfuhgr1v0e  28501  gsumpart  32195  esum2dlem  33079  esum2d  33080  esumiun  33081  carsgclctunlem1  33305  eulerpartlemgs2  33368  bnj1452  34052  fobigcup  34861  elsingles  34879  fnsingle  34880  fvsingle  34881  dfiota3  34884  funpartlem  34903  altxpsspw  34938  bj-snsetex  35833  bj-elsngl  35838  f1omptsnlem  36206  mptsnunlem  36208  topdifinffinlem  36217  heiborlem3  36670  ispointN  38602  mzpincl  41458  mzpcompact2lem  41475  pwslnmlem1  41820  pwslnm  41822  mpct  43886  salexct3  45045  salgencntex  45046  salgensscntex  45047  sge0xp  45132  mpoexxg2  46967