Theorem vsnex 5406

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 5405	. 2 ⊢ {𝑥, 𝑥} ∈ V
3	1, 2	eqeltri 2859	1 ⊢ {𝑥} ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455  {csn 4589  {cpr 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-sn 4590  df-pr 4592

This theorem is referenced by:  snexgALT  5412  rext  5429  sspwb  5430  moabex  5439  moabexOLD  5440  nnullss  5443  exss  5444  xpsspw  5796  funopg  6570  snnex  7753  soex  7914  opabex3d  7958  opabex3rd  7959  opabex3  7960  fo1st  8002  fo2nd  8003  mpoexxg  8068  cnvf1o  8102  sexp2  8138  sexp3  8145  naddcllem  8658  domunsn  9111  fodomr  9112  findcard2  9145  pwfilem  9273  marypha1lem  9389  brwdom2  9531  unxpwdom2  9546  elirrvOLDOLD  9557  epfrs  9696  dfac5lem2  10104  dfac5lem3  10105  dfac5lem4  10106  kmlem2  10131  isfin1-3  10365  hsmexlem4  10408  axcc2lem  10415  canthwe  10631  canthp1lem1  10632  uniwun  10720  rankcf  10757  hashmap  14468  hashbclem  14485  incexclem  15886  isfunc  17916  homaf  18082  symgvalstruct  19462  gsum2d2  20039  gsumcom2  20040  dprd2da  20109  mpfind  22266  pf1ind  22515  dishaus  23539  discmp  23555  dis2ndc  23617  dislly  23654  dis1stc  23656  unisngl  23684  1stckgen  23711  ptcmpfi  23970  isufil2  24065  cnextfval  24219  conway  27972  etaslts  27986  cofcutr  28117  istrkg2ld  28729  lfuhgr1v0e  29604  gsumpart  33383  gsumwrd2dccat  33398  esum2dlem  34482  esum2d  34483  esumiun  34484  carsgclctunlem1  34707  eulerpartlemgs2  34770  bnj1452  35440  fobigcup  36390  elsingles  36408  fnsingle  36409  fvsingle  36410  dfiota3  36413  funpartlem  36434  altxpsspw  36469  axtco  36982  ttcid  37003  ttcmin  37007  dfttc4lem2  37040  mh-inf3sn  37053  mh-infprim2bi  37058  bj-snsetex  37599  bj-elsngl  37604  f1omptsnlem  37982  mptsnunlem  37984  topdifinffinlem  37993  heiborlem3  38464  ispointN  40516  mzpincl  43465  mzpcompact2lem  43482  pwslnmlem1  43819  pwslnm  43821  permaxinf2lem  45721  mpct  45918  salexct3  47056  salgencntex  47057  salgensscntex  47058  sge0xp  47143  clnbgrval  48587  mpoexxg2  49118  tposideq  49666  discsntermlem  50348