Theorem eleqtri 2909

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtri.1	⊢ 𝐴 ∈ 𝐵
eleqtri.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eleqtri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtri

Step	Hyp	Ref	Expression
1		eleqtri.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtri.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	eleq2i 2902	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)
4	1, 3	mpbi 232	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2813  df-clel 2891

This theorem is referenced by:  eleqtrri  2910  3eltr3i  2923  prid2  4680  2eluzge0  12275  fz0to4untppr  12995  seqp1i  13371  faclbnd4lem1  13638  cats1fv  14201  bpoly2  15391  bpoly3  15392  bpoly4  15393  ef0lem  15412  phi1  16088  gsumws1  17980  lt6abl  18993  uvcvvcl  20909  smadiadetlem4  21256  indiscld  21677  cnrehmeo  23535  ovolicc1  24095  dvcjbr  24526  vieta1lem2  24881  dvloglem  25212  logdmopn  25213  efopnlem2  25221  cxpcn  25307  loglesqrt  25320  log2ublem2  25506  efrlim  25528  tgcgr4  26298  axlowdimlem16  26724  axlowdimlem17  26725  nlelchi  29817  hmopidmchi  29907  raddcn  31174  xrge0tmd  31190  indf  31276  ballotlem1ri  31794  chtvalz  31902  circlemethhgt  31916  dvtanlem  34970  ftc1cnnc  34993  dvasin  35005  dvacos  35006  dvreasin  35007  dvreacos  35008  areacirclem2  35010  areacirclem4  35012  cncfres  35070  jm2.23  39680  fvnonrel  40042  frege54cor1c  40346  fourierdlem28  42505  fourierdlem57  42533  fourierdlem59  42535  fourierdlem62  42538  fourierdlem68  42544  fouriersw  42601  etransclem23  42627  etransclem35  42639  etransclem38  42642  etransclem39  42643  etransclem44  42648  etransclem45  42649  etransclem47  42651  rrxtopn0  42663  hoidmvlelem2  42963  vonicclem2  43051  fmtno4prmfac  43814