Theorem eleqtri 2858

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

This proof depends on syntax axioms:   = wceq 1569   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835

This theorem is used by:  eleqtrri  2859  3eltr3i  2872  prid2  4723  indf  12326  2eluzge0  13008  faclbnd4lem1  14437  cats1fv  15010  bpoly2  16223  bpoly3  16224  bpoly4  16225  ef0lem  16244  phi1  16950  gsumws1  19034  lt6abl  20109  uvcvvcl  22093  mhpvarcl  22469  smadiadetlem4  22984  indiscld  23409  cnrehmeo  25274  ovolicc1  25837  dvcjbr  26269  vieta1lem2  26634  dvloglem  26976  logdmopn  26977  efopnlem2  26985  cxpcn  27073  loglesqrt  27089  log2ublem2  27275  efrlim  27297  precsexlem11  28603  tgcgr4  28994  axlowdimlem16  29535  axlowdimlem17  29536  nlelchi  32663  hmopidmchi  32753  evl1deg2  34109  evl1deg3  34110  esplyfvaln  34206  raddcn  34561  xrge0tmd  34577  ballotlem1ri  35167  chtvalz  35258  circlemethhgt  35272  dvtanlem  38588  ftc1cnnc  38611  dvasin  38623  dvacos  38624  dvreasin  38625  dvreacos  38626  areacirclem2  38628  areacirclem4  38630  cncfres  38700  resuppsinopn  43415  jm2.23  44003  0finon  44449  1finon  44450  2finon  44451  3finon  44452  4finon  44453  fvnonrel  44597  frege54cor1c  44915  fourierdlem28  47145  fourierdlem57  47173  fourierdlem59  47175  fourierdlem62  47178  fourierdlem68  47184  fouriersw  47241  etransclem23  47267  etransclem35  47279  etransclem38  47282  etransclem39  47283  etransclem44  47288  etransclem45  47289  etransclem47  47291  rrxtopn0  47303  hoidmvlelem2  47606  vonicclem2  47694  fmtno4prmfac  48657  gpg5grlim  49191  gpg5grlic  49192  dvsec  50856  dvcsc  50857  dvcot  50858  veroquadgsumlem  50983