Theorem vsnex 5434

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 4639	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5433	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2837	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3480  {csn 4626  {cpr 4628

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  snexg  5435  rext  5453  sspwb  5454  moabex  5464  nnullss  5467  exss  5468  xpsspw  5819  funopg  6600  snnex  7778  soex  7943  opabex3d  7990  opabex3rd  7991  opabex3  7992  fo1st  8034  fo2nd  8035  mpoexxg  8100  cnvf1o  8136  sexp2  8171  sexp3  8178  naddcllem  8714  domunsn  9167  fodomr  9168  findcard2  9204  pwfilem  9356  marypha1lem  9473  brwdom2  9613  unxpwdom2  9628  elirrv  9636  epfrs  9771  dfac5lem2  10164  dfac5lem3  10165  dfac5lem4  10166  dfac5lem4OLD  10168  kmlem2  10192  isfin1-3  10426  hsmexlem4  10469  axcc2lem  10476  canthwe  10691  canthp1lem1  10692  uniwun  10780  rankcf  10817  hashmap  14474  hashbclem  14491  incexclem  15872  isfunc  17909  homaf  18075  symgvalstruct  19414  gsum2d2  19992  gsumcom2  19993  dprd2da  20062  mpfind  22131  pf1ind  22359  dishaus  23390  discmp  23406  dis2ndc  23468  dislly  23505  dis1stc  23507  unisngl  23535  1stckgen  23562  ptcmpfi  23821  isufil2  23916  cnextfval  24070  conway  27844  etasslt  27858  cofcutr  27958  lfuhgr1v0e  29271  gsumpart  33060  gsumwrd2dccat  33070  esum2dlem  34093  esum2d  34094  esumiun  34095  carsgclctunlem1  34319  eulerpartlemgs2  34382  bnj1452  35066  fobigcup  35901  elsingles  35919  fnsingle  35920  fvsingle  35921  dfiota3  35924  funpartlem  35943  altxpsspw  35978  bj-snsetex  36964  bj-elsngl  36969  f1omptsnlem  37337  mptsnunlem  37339  topdifinffinlem  37348  heiborlem3  37820  ispointN  39744  mzpincl  42745  mzpcompact2lem  42762  pwslnmlem1  43104  pwslnm  43106  mpct  45206  salexct3  46357  salgencntex  46358  salgensscntex  46359  sge0xp  46444  clnbgrval  47809  mpoexxg2  48254  tposideq  48788