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

Theorem eqbrtri 5054
Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)
Hypotheses
Ref Expression
eqbrtr.1 𝐴 = 𝐵
eqbrtr.2 𝐵𝑅𝐶
Assertion
Ref Expression
eqbrtri 𝐴𝑅𝐶

Proof of Theorem eqbrtri
StepHypRef Expression
1 eqbrtr.2 . 2 𝐵𝑅𝐶
2 eqbrtr.1 . . 3 𝐴 = 𝐵
32breq1i 5040 . 2 (𝐴𝑅𝐶𝐵𝑅𝐶)
41, 3mpbir 234 1 𝐴𝑅𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538   class class class wbr 5033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034
This theorem is referenced by:  eqbrtrri  5056  3brtr4i  5063  infxpenc2  9437  dju1p1e2  9588  pwsdompw  9619  r1om  9659  aleph1  9986  canthp1lem1  10067  neg1lt0  11746  halflt1  11847  3halfnz  12053  declei  12126  numlti  12127  sqlecan  13571  discr  13601  faclbnd3  13652  hashunlei  13786  hashge2el2dif  13838  geo2lim  15227  0.999...  15233  geoihalfsum  15234  cos2bnd  15537  sin4lt0  15544  eirrlem  15553  rpnnen2lem3  15565  rpnnen2lem9  15571  aleph1re  15594  1nprm  16017  strle2  16589  strle3  16590  1strstr  16594  2strstr  16598  rngstr  16615  srngstr  16623  lmodstr  16632  ipsstr  16639  phlstr  16649  topgrpstr  16657  otpsstr  16664  odrngstr  16675  imasvalstr  16721  0frgp  18901  cnfldstr  20097  zlmlem  20214  tnglem  23250  iscmet3lem3  23898  mbfimaopnlem  24263  mbfsup  24272  mbfi1fseqlem6  24328  aalioulem3  24934  aaliou3lem3  24944  dvradcnv  25020  asin1  25484  log2cnv  25534  log2tlbnd  25535  mule1  25737  bposlem5  25876  bposlem8  25879  zabsle1  25884  trkgstr  26242  0pth  27914  ex-fl  28236  blocnilem  28591  norm3difi  28934  norm3adifii  28935  bcsiALT  28966  nmopsetn0  29652  nmfnsetn0  29665  nmopge0  29698  nmfnge0  29714  0bdop  29780  nmcexi  29813  opsqrlem6  29932  dp2lt10  30590  dplti  30611  dpmul4  30620  idlsrgstr  31059  locfinref  31198  dya2iocct  31652  signswch  31945  hgt750lem  32036  hgt750lem2  32037  subfaclim  32549  logi  33080  faclim  33092  cnndvlem1  33990  taupilem2  34737  cntotbnd  35233  60gcd7e1  39292  diophren  39751  algstr  40118  pr2dom  40232  tr3dom  40233  binomcxplemnn0  41050  binomcxplemrat  41051  stirlinglem1  42713  dirkercncflem1  42742  fouriersw  42870  meaiunlelem  43104  nfermltl2rev  44258  evengpoap3  44314  exple2lt6  44763  nnlog2ge0lt1  44977
  Copyright terms: Public domain W3C validator