Theorem eleqtri 2848

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 2842	. 2 ⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ 𝐶)
4	1, 3	mpbi 220	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1631   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767

This theorem is referenced by:  eleqtrri  2849  3eltr3i  2862  prid2  4434  2eluzge0  11935  fz0to4untppr  12650  seqp1i  13024  faclbnd4lem1  13284  cats1fv  13813  bpoly2  14994  bpoly3  14995  bpoly4  14996  ef0lem  15015  phi1  15685  gsumws1  17584  lt6abl  18503  uvcvvcl  20343  smadiadetlem4  20694  indiscld  21116  cnrehmeo  22972  ovolicc1  23504  dvcjbr  23932  vieta1lem2  24286  dvloglem  24615  logdmopn  24616  efopnlem2  24624  cxpcn  24707  loglesqrt  24720  log2ublem2  24895  efrlim  24917  tgcgr4  25647  axlowdimlem16  26058  axlowdimlem17  26059  nlelchi  29260  hmopidmchi  29350  raddcn  30315  xrge0tmd  30332  indf  30417  ballotlem1ri  30936  chtvalz  31047  circlemethhgt  31061  dvtanlem  33791  ftc1cnnc  33816  dvasin  33828  dvacos  33829  dvreasin  33830  dvreacos  33831  areacirclem2  33833  areacirclem4  33835  cncfres  33896  jm2.23  38089  fvnonrel  38429  frege54cor1c  38735  fourierdlem28  40869  fourierdlem57  40897  fourierdlem59  40899  fourierdlem62  40902  fourierdlem68  40908  fouriersw  40965  etransclem23  40991  etransclem35  41003  etransclem38  41006  etransclem39  41007  etransclem44  41012  etransclem45  41013  etransclem47  41015  rrxtopn0  41030  hoidmvlelem2  41330  vonicclem2  41418  fmtno4prmfac  42012