Theorem vsnex 5449

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 4661	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5448	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2840	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488  {csn 4648  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  snexg  5450  rext  5468  sspwb  5469  moabex  5479  nnullss  5482  exss  5483  xpsspw  5833  funopg  6612  snnex  7793  soex  7961  opabex3d  8006  opabex3rd  8007  opabex3  8008  fo1st  8050  fo2nd  8051  mpoexxg  8116  cnvf1o  8152  sexp2  8187  sexp3  8194  naddcllem  8732  domunsn  9193  fodomr  9194  findcard2  9230  pwfilem  9384  marypha1lem  9502  brwdom2  9642  unxpwdom2  9657  elirrv  9665  epfrs  9800  dfac5lem2  10193  dfac5lem3  10194  dfac5lem4  10195  dfac5lem4OLD  10197  kmlem2  10221  isfin1-3  10455  hsmexlem4  10498  axcc2lem  10505  canthwe  10720  canthp1lem1  10721  uniwun  10809  rankcf  10846  hashmap  14484  hashbclem  14501  incexclem  15884  isfunc  17928  homaf  18097  symgvalstruct  19438  gsum2d2  20016  gsumcom2  20017  dprd2da  20086  mpfind  22154  pf1ind  22380  dishaus  23411  discmp  23427  dis2ndc  23489  dislly  23526  dis1stc  23528  unisngl  23556  1stckgen  23583  ptcmpfi  23842  isufil2  23937  cnextfval  24091  conway  27862  etasslt  27876  cofcutr  27976  lfuhgr1v0e  29289  gsumpart  33038  esum2dlem  34056  esum2d  34057  esumiun  34058  carsgclctunlem1  34282  eulerpartlemgs2  34345  bnj1452  35028  fobigcup  35864  elsingles  35882  fnsingle  35883  fvsingle  35884  dfiota3  35887  funpartlem  35906  altxpsspw  35941  bj-snsetex  36929  bj-elsngl  36934  f1omptsnlem  37302  mptsnunlem  37304  topdifinffinlem  37313  heiborlem3  37773  ispointN  39699  mzpincl  42690  mzpcompact2lem  42707  pwslnmlem1  43049  pwslnm  43051  mpct  45108  salexct3  46263  salgencntex  46264  salgensscntex  46265  sge0xp  46350  clnbgrval  47696  mpoexxg2  48062