Theorem vsnex 5377

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 4580	. 2 ⊢ {𝑥} = {𝑥, 𝑥}
2		zfpair2 5376	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2832	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  {csn 4567  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  snexgALT  5383  rext  5400  sspwb  5401  moabex  5410  moabexOLD  5411  nnullss  5414  exss  5415  xpsspw  5765  funopg  6532  snnex  7712  soex  7872  opabex3d  7918  opabex3rd  7919  opabex3  7920  fo1st  7962  fo2nd  7963  mpoexxg  8028  cnvf1o  8061  sexp2  8096  sexp3  8103  naddcllem  8612  domunsn  9065  fodomr  9066  findcard2  9099  pwfilem  9228  marypha1lem  9346  brwdom2  9488  unxpwdom2  9503  elirrvOLD  9513  epfrs  9652  dfac5lem2  10046  dfac5lem3  10047  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem2  10074  isfin1-3  10308  hsmexlem4  10351  axcc2lem  10358  canthwe  10574  canthp1lem1  10575  uniwun  10663  rankcf  10700  hashmap  14397  hashbclem  14414  incexclem  15801  isfunc  17831  homaf  17997  symgvalstruct  19372  gsum2d2  19949  gsumcom2  19950  dprd2da  20019  mpfind  22093  pf1ind  22320  dishaus  23347  discmp  23363  dis2ndc  23425  dislly  23462  dis1stc  23464  unisngl  23492  1stckgen  23519  ptcmpfi  23778  isufil2  23873  cnextfval  24027  conway  27771  etaslts  27785  cofcutr  27916  istrkg2ld  28528  lfuhgr1v0e  29323  gsumpart  33124  gsumwrd2dccat  33139  esum2dlem  34236  esum2d  34237  esumiun  34238  carsgclctunlem1  34461  eulerpartlemgs2  34524  bnj1452  35194  fobigcup  36080  elsingles  36098  fnsingle  36099  fvsingle  36100  dfiota3  36103  funpartlem  36124  altxpsspw  36159  axtco  36653  ttcid  36674  ttcmin  36678  dfttc4lem2  36711  mh-inf3sn  36724  mh-infprim2bi  36729  bj-snsetex  37270  bj-elsngl  37275  f1omptsnlem  37652  mptsnunlem  37654  topdifinffinlem  37663  heiborlem3  38134  ispointN  40188  mzpincl  43166  mzpcompact2lem  43183  pwslnmlem1  43520  pwslnm  43522  permaxinf2lem  45439  mpct  45630  salexct3  46770  salgencntex  46771  salgensscntex  46772  sge0xp  46857  clnbgrval  48298  mpoexxg2  48814  tposideq  49363  discsntermlem  50045