Theorem vsnex 5392

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 4605	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5391	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2825	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3450  {csn 4592  {cpr 4594

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 2702  ax-sep 5254  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  snexg  5393  rext  5411  sspwb  5412  moabex  5422  nnullss  5425  exss  5426  xpsspw  5775  funopg  6553  snnex  7737  soex  7900  opabex3d  7947  opabex3rd  7948  opabex3  7949  fo1st  7991  fo2nd  7992  mpoexxg  8057  cnvf1o  8093  sexp2  8128  sexp3  8135  naddcllem  8643  domunsn  9097  fodomr  9098  findcard2  9134  pwfilem  9274  marypha1lem  9391  brwdom2  9533  unxpwdom2  9548  elirrv  9556  epfrs  9691  dfac5lem2  10084  dfac5lem3  10085  dfac5lem4  10086  dfac5lem4OLD  10088  kmlem2  10112  isfin1-3  10346  hsmexlem4  10389  axcc2lem  10396  canthwe  10611  canthp1lem1  10612  uniwun  10700  rankcf  10737  hashmap  14407  hashbclem  14424  incexclem  15809  isfunc  17833  homaf  17999  symgvalstruct  19334  gsum2d2  19911  gsumcom2  19912  dprd2da  19981  mpfind  22021  pf1ind  22249  dishaus  23276  discmp  23292  dis2ndc  23354  dislly  23391  dis1stc  23393  unisngl  23421  1stckgen  23448  ptcmpfi  23707  isufil2  23802  cnextfval  23956  conway  27718  etasslt  27732  cofcutr  27839  lfuhgr1v0e  29188  gsumpart  33004  gsumwrd2dccat  33014  esum2dlem  34089  esum2d  34090  esumiun  34091  carsgclctunlem1  34315  eulerpartlemgs2  34378  bnj1452  35049  fobigcup  35895  elsingles  35913  fnsingle  35914  fvsingle  35915  dfiota3  35918  funpartlem  35937  altxpsspw  35972  bj-snsetex  36958  bj-elsngl  36963  f1omptsnlem  37331  mptsnunlem  37333  topdifinffinlem  37342  heiborlem3  37814  ispointN  39743  mzpincl  42729  mzpcompact2lem  42746  pwslnmlem1  43088  pwslnm  43090  permaxinf2lem  45009  mpct  45202  salexct3  46347  salgencntex  46348  salgensscntex  46349  sge0xp  46434  clnbgrval  47827  mpoexxg2  48330  tposideq  48880  discsntermlem  49563