Theorem eqbrtrrd 5099

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 24-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrrd.2	⊢ (𝜑 → 𝐴𝑅𝐶)

Assertion

Ref	Expression
eqbrtrrd	⊢ (𝜑 → 𝐵𝑅𝐶)

Proof of Theorem eqbrtrrd

Step	Hyp	Ref	Expression
1		eqbrtrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2745	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 5097	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  dftpos4  8070  dif1en  8954  fodomfi  9101  resfifsupp  9165  cnfcom2lem  9468  dmttrcl  9488  ttrclselem2  9493  ficardadju  9964  enfin1ai  10149  pwcfsdom  10348  fpwwe2lem6  10401  fpwwe2  10408  canthp1lem1  10417  1nqenq  10727  prlem936  10812  lemulge11  11846  supaddc  11951  supmul1  11953  mul2lt0llt0  12843  mul2lt0lgt0  12844  xaddge0  13001  xadddi2  13040  ltexp2a  13893  leexp2a  13899  nnlesq  13931  digit1  13961  faclbnd4lem1  14016  faclbnd6  14022  facavg  14024  prsshashgt1  14134  nehash2  14197  abs3dif  15052  abs2dif  15053  limsupgre  15199  rlimclim1  15263  rlimuni  15268  rlimres2  15279  rlimcn1  15306  rlimcn1b  15307  recn2  15319  imcn2  15320  rlimo1  15335  o1rlimmul  15337  iserex  15377  isercoll  15388  caucvgrlem2  15395  caucvgr  15396  iseraltlem3  15404  summolem2a  15436  fsumge1  15518  o1fsum  15534  isumrpcl  15564  climcnds  15572  harmonic  15580  mertenslem1  15605  prodmolem2a  15653  ege2le3  15808  efgt1p2  15832  efgt1p  15833  eirrlem  15922  rpnnen2lem11  15942  fsumdvds  16026  bitsfzo  16151  bitsmod  16152  bitscmp  16154  mulgcd  16265  dvdssqlem  16280  nn0seqcvgd  16284  mulgcddvds  16369  rpdvds  16374  qden1elz  16470  phimullem  16489  hashgcdlem  16498  hashgcdeq  16499  pcdvdstr  16586  pockthg  16616  prmreclem1  16626  4sqlem11  16665  ramub1lem1  16736  ramub1lem2  16737  mreexexlem4d  17365  sscid  17545  latmlej21  18207  latmlej22  18208  lubel  18241  efginvrel1  19343  odadd2  19459  odadd  19460  gexexlem  19462  cyggex2  19507  ablfacrplem  19677  ablfac1c  19683  ablfac1eu  19685  pgpfac1lem3a  19688  isabvd  20089  mptscmfsuppd  20198  znrrg  20782  frlmphl  20997  frlmup1  21014  f1linds  21041  chcoeffeqlem  22043  lmcn2  22809  metrtri  23519  imasdsf1olem  23535  stdbdxmet  23680  nrmmetd  23739  nmmtri  23787  nlmvscnlem2  23858  blcvx  23970  recld2  23986  zdis  23988  opnreen  24003  cnheibor  24127  lebnumlem3  24135  nmoleub2lem3  24287  nmoleub2lem2  24288  nmoleub3  24291  ipcnlem2  24417  cmetcaulem  24461  nglmle  24475  cncmet  24495  csbren  24572  trirn  24573  minveclem4  24605  ovoliunlem1  24675  ovoliun2  24679  ovolscalem1  24686  ovolicopnf  24697  voliunlem2  24724  volsup  24729  ioorcl2  24745  uniiccvol  24753  uniioombllem4  24759  i1fd  24854  mbfi1fseqlem4  24892  itg2const2  24915  itg2eqa  24919  itg2split  24923  itg2i1fseqle  24928  itg2cnlem2  24936  dvcnv  25150  dveflem  25152  dvferm1lem  25157  dvlip2  25168  c1liplem1  25169  dvivthlem1  25181  lhop1lem  25186  dvcvx  25193  dvfsumle  25194  dvfsumabs  25196  dvfsumlem4  25202  dvfsumrlim2  25205  ftc1a  25210  tdeglem4  25233  tdeglem4OLD  25234  deg1pwle  25293  fta1blem  25342  aalioulem3  25503  aaliou2b  25510  ulmbdd  25566  ulmdvlem1  25568  itgulm  25576  pserdvlem2  25596  abelthlem3  25601  abelthlem5  25603  abelthlem6  25604  abelthlem7  25606  tanregt0  25704  argimlt0  25777  logdivlti  25784  logcnlem3  25808  logcnlem4  25809  logtayl  25824  logtayl2  25826  cxple2  25861  cxpcn3lem  25909  cxpaddle  25914  isosctrlem1  25977  atantayl  26096  efrlim  26128  dfef2  26129  o1cxp  26133  cxp2lim  26135  divsqrtsumo1  26142  amgmlem  26148  logdifbnd  26152  emcllem7  26160  harmonicbnd4  26169  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamucov  26196  lgamcvg2  26213  gamcvg2  26218  ftalem2  26232  basellem2  26240  basellem5  26243  basellem9  26247  vma1  26324  sqff1o  26340  fsumfldivdiaglem  26347  chtub  26369  fsumvma2  26371  chpchtsum  26376  chpub  26377  logfaclbnd  26379  logfacbnd3  26380  logfacrlim  26381  logexprlim  26382  bcmono  26434  bposlem2  26442  bposlem5  26445  bposlem6  26446  lgsne0  26492  lgsquadlem1  26537  lgsquadlem2  26538  2sqblem  26588  2sqmod  26593  chebbnd1lem1  26626  chtppilimlem1  26630  chtppilimlem2  26631  chpchtlim  26636  rplogsumlem1  26641  dchrvmasumiflem1  26658  dchrisum0flblem2  26666  dchrisum0fno1  26668  dchrisum0lem2a  26674  dchrisum0lem3  26676  dirith  26686  mulog2sumlem1  26691  mulog2sumlem2  26692  log2sumbnd  26701  selberglem2  26703  logdivbnd  26713  selberg3lem1  26714  selberg4lem1  26717  pntrsumbnd2  26724  pntrlog2bndlem1  26734  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem3  26749  pntlemb  26754  pntlemn  26757  pntlemr  26759  pntlemj  26760  pntlemf  26762  pntlemo  26764  ostth2lem3  26792  ostth3  26795  footeq  27094  hlperpnel  27095  perpdragALT  27097  perpdrag  27098  colperp  27099  mideulem2  27104  opphllem  27105  opphllem3  27119  lmieu  27154  trgcopy  27174  sacgr  27201  acopyeu  27204  usgredgleordALT  27610  eucrctshift  28616  nvabs  29043  smcnlem  29068  ubthlem2  29242  minvecolem4  29251  htthlem  29288  normpyc  29517  nmophmi  30402  hstle  30601  hstles  30602  stlei  30611  f1rnen  30973  fmptssfisupp  31028  nnmulge  31082  fsumiunle  31152  wrdt2ind  31234  xrge0npcan  31312  trsp2cyc  31399  archirngz  31452  archiabllem1a  31454  archiabllem2a  31457  archiabllem2c  31458  ornglmulle  31513  orngrmulle  31514  drngdimgt0  31710  lbsdiflsp0  31716  madjusmdetlem2  31787  esumpinfval  32050  esumpinfsum  32054  esumpcvgval  32055  esum2d  32070  esumiun  32071  dya2icoseg  32253  omssubadd  32276  carsgsigalem  32291  carsggect  32294  carsgclctunlem3  32296  omsmeas  32299  eulerpartlems  32336  sgnmulsgn  32525  signsplypnf  32538  signsply0  32539  reprlt  32608  reprinfz1  32611  hgt750lemc  32636  hgt750lemf  32642  pthhashvtx  33098  resconn  33217  sinccvglem  33639  circum  33641  btwnxfr  34367  nn0prpwlem  34520  dnibndlem2  34668  unblimceq0  34696  irrdiff  35506  poimirlem7  35793  mblfinlem3  35825  mblfinlem4  35826  itg2addnclem3  35839  ftc1anc  35867  isbnd3  35951  cntotbnd  35963  bfp  35991  rrndstprj2  35998  1cvrjat  37496  3atlem1  37504  3atlem6  37509  llnmlplnN  37560  2llnjaN  37587  2lplnja  37640  dalem57  37750  dalawlem11  37902  dalawlem12  37903  lhp2lt  38022  lhpj1  38043  lhpm0atN  38050  4atexlemex2  38092  lautm  38115  cdleme17b  38308  cdleme20j  38339  cdleme30a  38399  cdlemg4c  38633  cdlemg17a  38682  cdlemg31c  38720  trljco  38761  cdlemk46  38969  dia2dimlem2  39086  cdlemm10N  39139  cdlemn10  39227  dihmeetlem1N  39311  dihglblem5apreN  39312  dihmeetlem15N  39342  mapdat  39688  lcmineqlem19  40062  lcmineqlem20  40063  aks4d1p1p5  40090  aks4d1p8d2  40100  aks4d1p8  40102  aks4d1p9  40103  metakunt29  40160  2xp3dxp2ge1d  40169  factwoffsmonot  40170  mhphflem  40291  dvdsexpnn  40347  rtprmirr  40354  fltnlta  40507  3cubeslem1  40513  irrapxlem1  40651  irrapxlem4  40654  pell1qrgaplem  40702  pellfundglb  40714  rmspecfund  40738  monotoddzzfi  40771  rmynn  40785  jm2.24nn  40788  jm2.17c  40791  jm2.24  40792  acongeq  40812  jm2.20nn  40826  jm2.26lem3  40830  jm2.27a  40834  jm2.27c  40836  rmydioph  40843  jm3.1lem2  40847  frlmpwfi  40930  areaquad  41054  rp-isfinite6  41132  frege129d  41378  leeq1d  41774  imo72b2  41790  cvgdvgrat  41938  radcnvrat  41939  hashnzfzclim  41947  isosctrlem1ALT  42561  cncmpmax  42582  iooabslt  43044  fmul01lt1lem2  43133  clim1fr1  43149  limcrecl  43177  climxrrelem  43297  liminflbuz2  43363  stoweidlem1  43549  stoweidlem11  43559  stoweidlem14  43562  stoweidlem24  43572  stoweidlem26  43574  wallispilem4  43616  wallispilem5  43617  stirlinglem1  43622  fourierdlem51  43705  fourierdlem65  43719  fouriersw  43779  2leaddle2  44801  sqrtpwpw2p  45001  lighneallem4a  45071  flnn0div2ge  45890  logbpw2m1  45924  amgmwlem  46517