Theorem eqbrtrrd 5120

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-br 5097

This theorem is referenced by:  dftpos4  8185  dif1en  9084  fodomfi  9210  fodomfiOLD  9228  fmptssfisupp  9295  resfifsupp  9298  cnfcom2lem  9608  dmttrcl  9628  ttrclselem2  9633  ficardadju  10108  enfin1ai  10292  pwcfsdom  10492  fpwwe2lem6  10545  fpwwe2  10552  canthp1lem1  10561  1nqenq  10871  prlem936  10956  lemulge11  12002  supaddc  12107  supmul1  12109  mul2lt0llt0  13009  mul2lt0lgt0  13010  xaddge0  13171  xadddi2  13210  ltexp2a  14087  leexp2a  14093  nnlesq  14126  digit1  14158  faclbnd4lem1  14214  faclbnd6  14220  facavg  14222  prsshashgt1  14331  nehash2  14395  abs3dif  15253  abs2dif  15254  limsupgre  15402  rlimclim1  15466  rlimuni  15471  rlimres2  15482  rlimcn1  15509  rlimcn1b  15510  recn2  15522  imcn2  15523  rlimo1  15538  o1rlimmul  15540  iserex  15578  isercoll  15589  caucvgrlem2  15596  caucvgr  15597  iseraltlem3  15605  summolem2a  15636  fsumge1  15718  o1fsum  15734  isumrpcl  15764  climcnds  15772  harmonic  15780  mertenslem1  15805  prodmolem2a  15855  ege2le3  16011  efgt1p2  16037  efgt1p  16038  eirrlem  16127  rpnnen2lem11  16147  fsumdvds  16233  bitsfzo  16360  bitsmod  16361  bitscmp  16363  mulgcd  16473  dvdssqlem  16491  nn0seqcvgd  16495  mulgcddvds  16580  rpdvds  16585  qden1elz  16682  phimullem  16704  hashgcdlem  16713  hashgcdeq  16715  pcdvdstr  16802  pockthg  16832  prmreclem1  16842  4sqlem11  16881  ramub1lem1  16952  ramub1lem2  16953  mreexexlem4d  17568  sscid  17746  latmlej21  18401  latmlej22  18402  lubel  18435  efginvrel1  19655  odadd2  19776  odadd  19777  gexexlem  19779  cyggex2  19824  ablfacrplem  19994  ablfac1c  20000  ablfac1eu  20002  pgpfac1lem3a  20005  isabvd  20743  ornglmulle  20798  orngrmulle  20799  mptscmfsuppd  20877  znrrg  21518  frlmphl  21734  frlmup1  21751  f1linds  21778  psdmplcl  22103  chcoeffeqlem  22827  lmcn2  23591  metrtri  24299  imasdsf1olem  24315  stdbdxmet  24457  nrmmetd  24516  nmmtri  24564  nlmvscnlem2  24627  blcvx  24740  recld2  24757  zdis  24759  opnreen  24774  cnheibor  24908  lebnumlem3  24916  nmoleub2lem3  25069  nmoleub2lem2  25070  nmoleub3  25073  ipcnlem2  25198  cmetcaulem  25242  nglmle  25256  cncmet  25276  csbren  25353  trirn  25354  minveclem4  25386  ovoliunlem1  25457  ovoliun2  25461  ovolscalem1  25468  ovolicopnf  25479  voliunlem2  25506  volsup  25511  ioorcl2  25527  uniiccvol  25535  uniioombllem4  25541  i1fd  25636  mbfi1fseqlem4  25673  itg2const2  25696  itg2eqa  25700  itg2split  25704  itg2i1fseqle  25709  itg2cnlem2  25717  dvcnv  25935  dveflem  25937  dvferm1lem  25942  dvlip2  25954  c1liplem1  25955  dvivthlem1  25967  lhop1lem  25972  dvcvx  25979  dvfsumle  25980  dvfsumleOLD  25981  dvfsumabs  25983  dvfsumlem4  25990  dvfsumrlim2  25993  ftc1a  25998  tdeglem4  26019  deg1pwle  26079  fta1blem  26130  aalioulem3  26296  aaliou2b  26303  ulmbdd  26361  ulmdvlem1  26363  itgulm  26371  pserdvlem2  26392  abelthlem3  26397  abelthlem5  26399  abelthlem6  26400  abelthlem7  26402  tanregt0  26502  argimlt0  26576  logdivlti  26583  logcnlem3  26607  logcnlem4  26608  logtayl  26623  logtayl2  26625  cxple2  26660  cxpcn3lem  26711  cxpaddle  26716  rtprmirr  26724  isosctrlem1  26782  atantayl  26901  efrlim  26933  efrlimOLD  26934  dfef2  26935  o1cxp  26939  cxp2lim  26941  divsqrtsumo1  26948  amgmlem  26954  logdifbnd  26958  emcllem7  26966  harmonicbnd4  26975  fsumharmonic  26976  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamucov  27002  lgamcvg2  27019  gamcvg2  27024  ftalem2  27038  basellem2  27046  basellem5  27049  basellem9  27053  vma1  27130  sqff1o  27146  fsumfldivdiaglem  27153  chtub  27177  fsumvma2  27179  chpchtsum  27184  chpub  27185  logfaclbnd  27187  logfacbnd3  27188  logfacrlim  27189  logexprlim  27190  bcmono  27242  bposlem2  27250  bposlem5  27253  bposlem6  27254  lgsne0  27300  lgsquadlem1  27345  lgsquadlem2  27346  2sqblem  27396  2sqmod  27401  chebbnd1lem1  27434  chtppilimlem1  27438  chtppilimlem2  27439  chpchtlim  27444  rplogsumlem1  27449  dchrvmasumiflem1  27466  dchrisum0flblem2  27474  dchrisum0fno1  27476  dchrisum0lem2a  27482  dchrisum0lem3  27484  dirith  27494  mulog2sumlem1  27499  mulog2sumlem2  27500  log2sumbnd  27509  selberglem2  27511  logdivbnd  27521  selberg3lem1  27522  selberg4lem1  27525  pntrsumbnd2  27532  pntrlog2bndlem1  27542  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntibndlem3  27557  pntlemb  27562  pntlemn  27565  pntlemr  27567  pntlemj  27568  pntlemf  27570  pntlemo  27572  ostth2lem3  27600  ostth3  27603  addsuniflem  27971  sltp1d  27985  negsid  28010  negsunif  28024  negsleft  28027  mulsuniflem  28118  precsexlem9  28183  n0sge0  28298  zscut  28365  halfcut  28415  addhalfcut  28416  pw2cut2  28419  footeq  28745  hlperpnel  28746  perpdragALT  28748  perpdrag  28749  colperp  28750  mideulem2  28755  opphllem  28756  opphllem3  28770  lmieu  28805  trgcopy  28825  sacgr  28852  acopyeu  28855  usgredgleordALT  29256  eucrctshift  30267  nvabs  30696  smcnlem  30721  ubthlem2  30895  minvecolem4  30904  htthlem  30941  normpyc  31170  nmophmi  32055  hstle  32254  hstles  32255  stlei  32264  f1rnen  32655  nnmulge  32767  fsumiunle  32859  sgnmulsgn  32872  wrdt2ind  32984  xrge0npcan  33051  gsumwrd2dccat  33109  trsp2cyc  33154  archirngz  33220  archiabllem1a  33222  archiabllem2a  33225  archiabllem2c  33226  elrgspnlem1  33273  elrgspn  33277  elrgspnsubrunlem2  33279  rprmasso  33555  q1pdir  33633  r1pquslmic  33641  evlextv  33656  mplvrpmga  33659  mplvrpmrhm  33661  drngdimgt0  33724  lbsdiflsp0  33732  fldextrspundgle  33784  fldext2rspun  33788  minplyirredlem  33816  madjusmdetlem2  33934  esumpinfval  34179  esumpinfsum  34183  esumpcvgval  34184  esum2d  34199  esumiun  34200  dya2icoseg  34383  omssubadd  34406  carsgsigalem  34421  carsggect  34424  carsgclctunlem3  34426  omsmeas  34429  eulerpartlems  34466  signsplypnf  34656  signsply0  34657  reprlt  34725  reprinfz1  34728  hgt750lemc  34753  hgt750lemf  34759  pthhashvtx  35271  resconn  35389  sinccvglem  35815  circum  35817  btwnxfr  36199  nn0prpwlem  36465  dnibndlem2  36622  unblimceq0  36650  irrdiff  37470  poimirlem7  37767  mblfinlem3  37799  mblfinlem4  37800  itg2addnclem3  37813  ftc1anc  37841  isbnd3  37924  cntotbnd  37936  bfp  37964  rrndstprj2  37971  1cvrjat  39674  3atlem1  39682  3atlem6  39687  llnmlplnN  39738  2llnjaN  39765  2lplnja  39818  dalem57  39928  dalawlem11  40080  dalawlem12  40081  lhp2lt  40200  lhpj1  40221  lhpm0atN  40228  4atexlemex2  40270  lautm  40293  cdleme17b  40486  cdleme20j  40517  cdleme30a  40577  cdlemg4c  40811  cdlemg17a  40860  cdlemg31c  40898  trljco  40939  cdlemk46  41147  dia2dimlem2  41264  cdlemm10N  41317  cdlemn10  41405  dihmeetlem1N  41489  dihglblem5apreN  41490  dihmeetlem15N  41520  mapdat  41866  lcmineqlem19  42240  lcmineqlem20  42241  aks4d1p1p5  42268  aks4d1p8d2  42278  aks4d1p8  42280  aks4d1p9  42281  hashscontpow  42315  dvdsexpnn  42530  mullt0b1d  42680  selvvvval  42770  evlselv  42772  mhphflem  42781  fltnlta  42848  3cubeslem1  42868  irrapxlem1  43006  irrapxlem4  43009  pell1qrgaplem  43057  pellfundglb  43069  rmspecfund  43093  monotoddzzfi  43126  rmynn  43140  jm2.24nn  43143  jm2.17c  43146  jm2.24  43147  acongeq  43167  jm2.20nn  43181  jm2.26lem3  43185  jm2.27a  43189  jm2.27c  43191  rmydioph  43198  jm3.1lem2  43202  frlmpwfi  43282  areaquad  43400  cantnf2  43509  rp-isfinite6  43701  frege129d  43946  leeq1d  44340  imo72b2lem0  44348  imo72b2  44355  cvgdvgrat  44496  radcnvrat  44497  hashnzfzclim  44505  isosctrlem1ALT  45116  cncmpmax  45219  iooabslt  45687  fmul01lt1lem2  45773  clim1fr1  45789  limcrecl  45817  climxrrelem  45935  liminflbuz2  46001  dvnprodlem1  46132  stoweidlem1  46187  stoweidlem11  46197  stoweidlem14  46200  stoweidlem24  46210  stoweidlem26  46212  wallispilem4  46254  wallispilem5  46255  stirlinglem1  46260  fourierdlem51  46343  fourierdlem65  46357  fouriersw  46417  2leaddle2  47486  sqrtpwpw2p  47726  lighneallem4a  47796  flnn0div2ge  48721  logbpw2m1  48755  functermclem  49694  amgmwlem  49989