MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleqtri Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 eleqtri.1 . 2 𝐴𝐵
2 eleqtri.2 . . 3 𝐵 = 𝐶
32eleq2i 2842 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 220 1 𝐴𝐶
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator