Theorem vsnex 5389

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 4602	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5388	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2824	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447  {csn 4589  {cpr 4591

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 5251  ax-pr 5387

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 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  snexg  5390  rext  5408  sspwb  5409  moabex  5419  nnullss  5422  exss  5423  xpsspw  5772  funopg  6550  snnex  7734  soex  7897  opabex3d  7944  opabex3rd  7945  opabex3  7946  fo1st  7988  fo2nd  7989  mpoexxg  8054  cnvf1o  8090  sexp2  8125  sexp3  8132  naddcllem  8640  domunsn  9091  fodomr  9092  findcard2  9128  pwfilem  9267  marypha1lem  9384  brwdom2  9526  unxpwdom2  9541  elirrv  9549  epfrs  9684  dfac5lem2  10077  dfac5lem3  10078  dfac5lem4  10079  dfac5lem4OLD  10081  kmlem2  10105  isfin1-3  10339  hsmexlem4  10382  axcc2lem  10389  canthwe  10604  canthp1lem1  10605  uniwun  10693  rankcf  10730  hashmap  14400  hashbclem  14417  incexclem  15802  isfunc  17826  homaf  17992  symgvalstruct  19327  gsum2d2  19904  gsumcom2  19905  dprd2da  19974  mpfind  22014  pf1ind  22242  dishaus  23269  discmp  23285  dis2ndc  23347  dislly  23384  dis1stc  23386  unisngl  23414  1stckgen  23441  ptcmpfi  23700  isufil2  23795  cnextfval  23949  conway  27711  etasslt  27725  cofcutr  27832  lfuhgr1v0e  29181  gsumpart  32997  gsumwrd2dccat  33007  esum2dlem  34082  esum2d  34083  esumiun  34084  carsgclctunlem1  34308  eulerpartlemgs2  34371  bnj1452  35042  fobigcup  35888  elsingles  35906  fnsingle  35907  fvsingle  35908  dfiota3  35911  funpartlem  35930  altxpsspw  35965  bj-snsetex  36951  bj-elsngl  36956  f1omptsnlem  37324  mptsnunlem  37326  topdifinffinlem  37335  heiborlem3  37807  ispointN  39736  mzpincl  42722  mzpcompact2lem  42739  pwslnmlem1  43081  pwslnm  43083  permaxinf2lem  45002  mpct  45195  salexct3  46340  salgencntex  46341  salgensscntex  46342  sge0xp  46427  clnbgrval  47823  mpoexxg2  48326  tposideq  48876  discsntermlem  49559