Theorem eqbrtrrd 5135

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 2769	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqbrtrrd.2	. 2 ⊢ (𝜑 → 𝐴𝑅𝐶)
4	2, 3	eqbrtrd 5133	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  dftpos4  8237  dif1en  9142  fodomfi  9268  fmptssfisupp  9350  cnfcom2lem  9666  dmttrcl  9686  ttrclselem2  9691  ficardadju  10179  enfin1ai  10363  pwcfsdom  10563  fpwwe2lem6  10616  fpwwe2  10623  canthp1lem1  10632  1nqenq  10942  prlem936  11027  lemulge11  12072  supaddc  12177  supmul1  12179  mul2lt0llt0  13117  mul2lt0lgt0  13118  xaddge0  13279  xadddi2  13318  ltexp2a  14198  leexp2a  14204  nnlesq  14237  digit1  14269  faclbnd4lem1  14325  faclbnd6  14331  facavg  14333  prsshashgt1  14443  nehash2  14507  sgnmulsgn  15142  abs3dif  15379  abs2dif  15380  limsupgre  15528  rlimclim1  15592  rlimuni  15597  rlimres2  15608  rlimcn1  15635  rlimcn1b  15636  recn2  15648  imcn2  15649  rlimo1  15664  o1rlimmul  15666  iserex  15704  isercoll  15715  caucvgrlem2  15722  caucvgr  15723  iseraltlem3  15731  summolem2a  15762  fsumge1  15845  o1fsum  15861  isumrpcl  15893  climcnds  15901  harmonic  15909  mertenslem1  15934  prodmolem2a  15984  ege2le3  16139  efgt1p2  16165  efgt1p  16166  eirrlem  16255  rpnnen2lem11  16275  fsumdvds  16361  bitsfzo  16488  bitsmod  16489  bitscmp  16491  mulgcd  16601  dvdssqlem  16619  nn0seqcvgd  16623  mulgcddvds  16708  rpdvds  16713  qden1elz  16811  phimullem  16833  hashgcdlem  16842  hashgcdeq  16844  pcdvdstr  16931  pockthg  16961  prmreclem1  16971  4sqlem11  17010  ramub1lem1  17081  ramub1lem2  17082  mreexexlem4d  17698  sscid  17876  latmlej21  18531  latmlej22  18532  lubel  18565  efginvrel1  19793  odadd2  19914  odadd  19915  gexexlem  19917  cyggex2  19962  ablfacrplem  20132  ablfac1c  20138  ablfac1eu  20140  pgpfac1lem3a  20143  isabvd  20915  ornglmulle  20970  orngrmulle  20971  mptscmfsuppd  21049  znrrg  21715  frlmphl  21931  frlmup1  21948  f1linds  21975  selvvvval  22293  psdmplcl  22325  chcoeffeqlem  23042  lmcn2  23806  metrtri  24514  imasdsf1olem  24530  stdbdxmet  24672  nrmmetd  24731  nmmtri  24779  nlmvscnlem2  24842  blcvx  24955  recld2  24972  zdis  24974  opnreen  24989  cnheibor  25114  lebnumlem3  25122  nmoleub2lem3  25274  nmoleub2lem2  25275  nmoleub3  25278  ipcnlem2  25403  cmetcaulem  25447  nglmle  25461  cncmet  25481  csbren  25558  trirn  25559  minveclem4  25591  ovoliunlem1  25661  ovoliun2  25665  ovolscalem1  25672  ovolicopnf  25683  voliunlem2  25710  volsup  25715  ioorcl2  25731  uniiccvol  25739  uniioombllem4  25745  i1fd  25840  mbfi1fseqlem4  25877  itg2const2  25900  itg2eqa  25904  itg2split  25908  itg2i1fseqle  25913  itg2cnlem2  25921  dvcnv  26136  dveflem  26138  dvferm1lem  26143  dvlip2  26154  c1liplem1  26155  dvivthlem1  26167  lhop1lem  26172  dvcvx  26179  dvfsumle  26180  dvfsumabs  26182  dvfsumlem4  26188  dvfsumrlim2  26191  ftc1a  26196  tdeglem4  26217  deg1pwle  26277  fta1blem  26328  aalioulem3  26497  aaliou2b  26504  ulmbdd  26561  ulmdvlem1  26563  itgulm  26571  pserdvlem2  26591  abelthlem3  26596  abelthlem5  26598  abelthlem6  26599  abelthlem7  26601  tanregt0  26704  argimlt0  26778  logdivlti  26785  logcnlem3  26809  logcnlem4  26810  logtayl  26825  logtayl2  26827  cxple2  26862  cxpcn3lem  26912  cxpaddle  26917  rtprmirr  26925  isosctrlem1  26983  atantayl  27102  efrlim  27134  dfef2  27135  o1cxp  27139  cxp2lim  27141  divsqrtsumo1  27148  amgmlem  27154  logdifbnd  27158  emcllem7  27166  harmonicbnd4  27175  fsumharmonic  27176  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamucov  27202  lgamcvg2  27219  gamcvg2  27224  ftalem2  27238  basellem2  27246  basellem5  27249  basellem9  27253  vma1  27330  sqff1o  27346  fsumfldivdiaglem  27353  chtub  27376  fsumvma2  27378  chpchtsum  27383  chpub  27384  logfaclbnd  27386  logfacbnd3  27387  logfacrlim  27388  logexprlim  27389  bcmono  27441  bposlem2  27449  bposlem5  27452  bposlem6  27453  lgsne0  27499  lgsquadlem1  27544  lgsquadlem2  27545  2sqblem  27595  2sqmod  27600  chebbnd1lem1  27633  chtppilimlem1  27637  chtppilimlem2  27638  chpchtlim  27643  rplogsumlem1  27648  dchrvmasumiflem1  27665  dchrisum0flblem2  27673  dchrisum0fno1  27675  dchrisum0lem2a  27681  dchrisum0lem3  27683  dirith  27693  mulog2sumlem1  27698  mulog2sumlem2  27699  log2sumbnd  27708  selberglem2  27710  logdivbnd  27720  selberg3lem1  27721  selberg4lem1  27724  pntrsumbnd2  27731  pntrlog2bndlem1  27741  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntibndlem3  27756  pntlemb  27761  pntlemn  27764  pntlemr  27766  pntlemj  27767  pntlemf  27769  pntlemo  27771  ostth2lem3  27799  ostth3  27802  addsuniflem  28194  ltsp1d  28208  negsid  28234  negsunif  28248  negleft  28251  mulsuniflem  28342  precsexlem9  28408  n0sge0  28531  zcuts  28600  halfcut  28651  addhalfcut  28652  pw2cut2  28655  bdayfinbndlem1  28660  footeq  29004  hlperpnel  29006  perpdragALT  29008  perpdrag  29009  colperp  29010  mideulem2  29015  opphllem  29016  opphllem3  29030  lmieu  29093  trgcopy  29115  sacgr  29142  acopyeu  29145  perpeqlem  29150  perpprlng  29200  prlngmid2  29211  usgredgleordALT  29584  eucrctshift  30594  nvabs  31024  smcnlem  31049  ubthlem2  31223  minvecolem4  31232  htthlem  31269  normpyc  31498  nmophmi  32383  hstle  32582  hstles  32583  stlei  32592  f1rnen  32973  nnmulge  33084  fsumiunle  33173  wrdt2ind  33273  xrge0npcan  33340  gsumwrd2dccat  33398  trsp2cyc  33443  archirngz  33509  archiabllem1a  33511  archiabllem2a  33514  archiabllem2c  33515  elrgspnlem1  33562  elrgspn  33566  elrgspnsubrunlem2  33568  rprmasso  33815  q1pdir  33893  r1pquslmic  33900  selvply1rhmlema  33908  selvply1rhmlem1  33910  evlextv  33932  mplvrpmga  33935  mplvrpmrhm  33937  drngdimgt0  34008  lbsdiflsp0  34016  fldextrspundgle  34068  fldext2rspun  34072  minplyirredlem  34100  madjusmdetlem2  34218  esumpinfval  34463  esumpinfsum  34467  esumpcvgval  34468  esum2d  34483  esumiun  34484  dya2icoseg  34667  omssubadd  34690  carsgsigalem  34705  carsggect  34708  carsgclctunlem3  34710  omsmeas  34713  eulerpartlems  34750  signsplypnf  34937  signsply0  34938  reprlt  35006  reprinfz1  35009  hgt750lemc  35034  hgt750lemf  35040  pthhashvtx  35620  resconn  35738  sinccvglem  36164  circum  36166  btwnxfr  36548  nn0prpwlem  36833  dnibndlem2  37068  unblimceq0  37096  irrdiff  37970  poimirlem7  38278  mblfinlem3  38310  mblfinlem4  38311  itg2addnclem3  38324  ftc1anc  38352  isbnd3  38435  cntotbnd  38447  bfp  38475  rrndstprj2  38482  1cvrjat  40249  3atlem1  40257  3atlem6  40262  llnmlplnN  40313  2llnjaN  40340  2lplnja  40393  dalem57  40503  dalawlem11  40655  dalawlem12  40656  lhp2lt  40775  lhpj1  40796  lhpm0atN  40803  4atexlemex2  40845  lautm  40868  cdleme17b  41061  cdleme20j  41092  cdleme30a  41152  cdlemg4c  41386  cdlemg17a  41435  cdlemg31c  41473  trljco  41514  cdlemk46  41722  dia2dimlem2  41839  cdlemm10N  41892  cdlemn10  41980  dihmeetlem1N  42064  dihglblem5apreN  42065  dihmeetlem15N  42095  mapdat  42441  lcmineqlem19  42814  lcmineqlem20  42815  aks4d1p1p5  42842  aks4d1p8d2  42852  aks4d1p8  42854  aks4d1p9  42855  hashscontpow  42889  dvdsexpnn  43094  mullt0b1d  43257  evlselv  43321  mhphflem  43328  fltnlta  43395  3cubeslem1  43415  irrapxlem1  43549  irrapxlem4  43552  pell1qrgaplem  43600  pellfundglb  43612  rmspecfund  43636  monotoddzzfi  43669  rmynn  43683  jm2.24nn  43686  jm2.17c  43689  jm2.24  43690  acongeq  43710  jm2.20nn  43724  jm2.26lem3  43728  jm2.27a  43732  jm2.27c  43734  rmydioph  43741  jm3.1lem2  43745  frlmpwfi  43825  areaquad  43943  cantnf2  44052  rp-isfinite6  44244  frege129d  44489  leeq1d  44883  imo72b2lem0  44891  imo72b2  44898  cvgdvgrat  45023  radcnvrat  45024  hashnzfzclim  45032  isosctrlem1ALT  45642  cncmpmax  45752  iooabslt  46215  fmul01lt1lem2  46301  clim1fr1  46317  limcrecl  46345  climxrrelem  46463  liminflbuz2  46529  dvnprodlem1  46660  stoweidlem1  46715  stoweidlem11  46725  stoweidlem14  46728  stoweidlem24  46738  stoweidlem26  46740  wallispilem4  46782  wallispilem5  46783  stirlinglem1  46788  fourierdlem51  46871  fourierdlem65  46885  fouriersw  46945  2leaddle2  48035  2timesltsqm1  48116  sqrtpwpw2p  48290  lighneallem4a  48360  flnn0div2ge  49313  logbpw2m1  49347  functermclem  50285  amgmwlem  50622