Theorem snidg 4621

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)

Assertion

Ref	Expression
snidg	⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})

Proof of Theorem snidg

Step	Hyp	Ref	Expression
1		eqid 2763	. 2 ⊢ 𝐴 = 𝐴
2		elsng 4598	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
3	1, 2	mpbiri 261	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sn 4589

This theorem is used by:  snidb  4622  elsn2g  4625  elinsn  4671  snnzg  4735  sneqrg  4797  selsALT  5414  intidg  5430  eldmressnsn  6026  elsnxp  6315  fsneq  7060  fvressn  7193  fnsnbg  7196  fvsnun1  7213  fsnunfv  7218  resf1extb  7973  1stconst  8141  2ndconst  8142  curry1  8145  curry2  8148  suppsnop  8226  mapsnd  8945  en1uniel  9088  dif1enlem  9206  unifpw  9375  sucprcregOLD  9631  djurf1o  10024  cfsuc  10365  elfzomin  13902  hashrabsn1  14548  swrds1  14847  fsumsplitsnun  15953  lcmfunsnlem1  16844  ramub1lem1  17236  basprssdmsets  17431  acsfiindd  18759  mgm1  18868  mnd1id  19006  odf1o1  19819  gsumconst  20181  lspsolv  21454  mat1ghm  22831  mat1mhm  22832  mavmul0  22900  m1detdiag  22945  mdetrlin  22950  mdetrsca  22951  chpmat1dlem  23186  maxlp  23498  cnpdis  23644  conncompid  23782  dislly  23849  locfindis  23882  dfac14lem  23969  txtube  23992  pt1hmeo  24158  ufileu  24271  filufint  24272  uffix  24273  uffixsn  24277  i1fima2sn  26034  ply1rem  26517  noextenddif  28058  noextendlt  28059  noextendgt  28060  cutlt  28351  addsval  28381  negsunif  28474  mulsval  28528  mulsproplem5  28539  mulsproplem6  28540  mulsproplem7  28541  mulsproplem8  28542  mulsuniflem  28568  lnincplng  29295  edglnl  29754  vtxd0nedgb  30102  1loopgrvd2  30117  wlkp1  30293  1wlkdlem2  30762  1conngr  30828  frgrwopregasn  30950  frgrwopregbsn  30951  wlkl0  31001  fconst7v  33289  elrspunsn  34063  selvply1rhmlemb  34234  mplmulmvr  34254  esplyind  34290  rtelextdg2  34442  esumel  34762  actfunsnrndisj  35317  reprsuc  35327  breprexplema  35342  derangsn  36115  erdszelem4  36139  cvmlift2lem9  36256  mirimanofffr  36642  fv1stcnv  36732  fv2ndcnv  36733  neibastop2lem  37339  ttcsnssg  37495  ttcsnidg  37496  bj-nsnid  38189  bj-snmoore  38238  ismrer1  38975  elpaddatriN  41063  frlmsnic  43808  kelac2  44271  rngunsnply  44374  brtrclfv2  44930  k0004lem3  45352  projf1o  46426  fsneqrn  46439  unirnmapsn  46442  ssmapsn  46444  fconst7  46491  mccllem  46824  limcresiooub  46867  limcresioolb  46868  cnfdmsn  47107  cxpcncf2  47124  dvmptfprodlem  47169  dvnprodlem1  47171  dvnprodlem2  47172  dvnprodlem3  47173  fourierdlem49  47380  prsal  47543  salexct  47559  salgencntex  47568  sge0sn  47604  sge0snmpt  47608  sge0snmptf  47662  caratheodorylem1  47751  hoiprodp1  47813  hoidmv1le  47819  hoidmvlelem1  47820  hoidmvlelem2  47821  hoidmvlelem3  47822  hoidmvlelem4  47823  hspmbllem2  47852  ovnovollem1  47881  ovnovollem2  47882  funressnfv  48328  cfsetsnfsetf  48343  cfsetsnfsetfo  48345  el1fzopredsuc  48611  snlindsntor  49798  lmod1lem1  49814  lmod1lem2  49815  lmod1lem3  49816  lmod1lem4  49817  lmod1lem5  49818  lmod1zr  49820  funcsn  50894