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 2828	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3473  {csn 4628  {cpr 4630

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  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  5809  funopg  6582  snnex  7749  soex  7916  opabex3d  7956  opabex3rd  7957  opabex3  7958  fo1st  7999  fo2nd  8000  mpoexxg  8066  cnvf1o  8102  sexp2  8137  sexp3  8144  naddcllem  8681  domunsn  9133  fodomr  9134  findcard2  9170  pwfilem  9183  marypha1lem  9434  brwdom2  9574  unxpwdom2  9589  elirrv  9597  epfrs  9732  dfac5lem2  10125  dfac5lem3  10126  dfac5lem4  10127  kmlem2  10152  isfin1-3  10387  hsmexlem4  10430  axcc2lem  10437  canthwe  10652  canthp1lem1  10653  uniwun  10741  rankcf  10778  hashmap  14402  hashbclem  14418  incexclem  15789  isfunc  17821  homaf  17990  symgvalstruct  19312  gsum2d2  19890  gsumcom2  19891  dprd2da  19960  mpfind  21981  pf1ind  22194  dishaus  23206  discmp  23222  dis2ndc  23284  dislly  23321  dis1stc  23323  unisngl  23351  1stckgen  23378  ptcmpfi  23637  isufil2  23732  cnextfval  23886  conway  27645  etasslt  27659  cofcutr  27757  lfuhgr1v0e  28944  gsumpart  32643  esum2dlem  33554  esum2d  33555  esumiun  33556  carsgclctunlem1  33780  eulerpartlemgs2  33843  bnj1452  34527  fobigcup  35342  elsingles  35360  fnsingle  35361  fvsingle  35362  dfiota3  35365  funpartlem  35384  altxpsspw  35419  bj-snsetex  36308  bj-elsngl  36313  f1omptsnlem  36681  mptsnunlem  36683  topdifinffinlem  36692  heiborlem3  37145  ispointN  39077  mzpincl  41935  mzpcompact2lem  41952  pwslnmlem1  42297  pwslnm  42299  mpct  44359  salexct3  45517  salgencntex  45518  salgensscntex  45519  sge0xp  45604  mpoexxg2  47176