Theorem eqbrtrrd 5113

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090

This theorem is referenced by:  dftpos4  8175  dif1en  9071  fodomfi  9196  fodomfiOLD  9214  fmptssfisupp  9278  resfifsupp  9281  cnfcom2lem  9591  dmttrcl  9611  ttrclselem2  9616  ficardadju  10091  enfin1ai  10275  pwcfsdom  10474  fpwwe2lem6  10527  fpwwe2  10534  canthp1lem1  10543  1nqenq  10853  prlem936  10938  lemulge11  11984  supaddc  12089  supmul1  12091  mul2lt0llt0  12996  mul2lt0lgt0  12997  xaddge0  13157  xadddi2  13196  ltexp2a  14073  leexp2a  14079  nnlesq  14112  digit1  14144  faclbnd4lem1  14200  faclbnd6  14206  facavg  14208  prsshashgt1  14317  nehash2  14381  abs3dif  15239  abs2dif  15240  limsupgre  15388  rlimclim1  15452  rlimuni  15457  rlimres2  15468  rlimcn1  15495  rlimcn1b  15496  recn2  15508  imcn2  15509  rlimo1  15524  o1rlimmul  15526  iserex  15564  isercoll  15575  caucvgrlem2  15582  caucvgr  15583  iseraltlem3  15591  summolem2a  15622  fsumge1  15704  o1fsum  15720  isumrpcl  15750  climcnds  15758  harmonic  15766  mertenslem1  15791  prodmolem2a  15841  ege2le3  15997  efgt1p2  16023  efgt1p  16024  eirrlem  16113  rpnnen2lem11  16133  fsumdvds  16219  bitsfzo  16346  bitsmod  16347  bitscmp  16349  mulgcd  16459  dvdssqlem  16477  nn0seqcvgd  16481  mulgcddvds  16566  rpdvds  16571  qden1elz  16668  phimullem  16690  hashgcdlem  16699  hashgcdeq  16701  pcdvdstr  16788  pockthg  16818  prmreclem1  16828  4sqlem11  16867  ramub1lem1  16938  ramub1lem2  16939  mreexexlem4d  17553  sscid  17731  latmlej21  18386  latmlej22  18387  lubel  18420  efginvrel1  19640  odadd2  19761  odadd  19762  gexexlem  19764  cyggex2  19809  ablfacrplem  19979  ablfac1c  19985  ablfac1eu  19987  pgpfac1lem3a  19990  isabvd  20727  ornglmulle  20782  orngrmulle  20783  mptscmfsuppd  20861  znrrg  21502  frlmphl  21718  frlmup1  21735  f1linds  21762  psdmplcl  22077  chcoeffeqlem  22800  lmcn2  23564  metrtri  24272  imasdsf1olem  24288  stdbdxmet  24430  nrmmetd  24489  nmmtri  24537  nlmvscnlem2  24600  blcvx  24713  recld2  24730  zdis  24732  opnreen  24747  cnheibor  24881  lebnumlem3  24889  nmoleub2lem3  25042  nmoleub2lem2  25043  nmoleub3  25046  ipcnlem2  25171  cmetcaulem  25215  nglmle  25229  cncmet  25249  csbren  25326  trirn  25327  minveclem4  25359  ovoliunlem1  25430  ovoliun2  25434  ovolscalem1  25441  ovolicopnf  25452  voliunlem2  25479  volsup  25484  ioorcl2  25500  uniiccvol  25508  uniioombllem4  25514  i1fd  25609  mbfi1fseqlem4  25646  itg2const2  25669  itg2eqa  25673  itg2split  25677  itg2i1fseqle  25682  itg2cnlem2  25690  dvcnv  25908  dveflem  25910  dvferm1lem  25915  dvlip2  25927  c1liplem1  25928  dvivthlem1  25940  lhop1lem  25945  dvcvx  25952  dvfsumle  25953  dvfsumleOLD  25954  dvfsumabs  25956  dvfsumlem4  25963  dvfsumrlim2  25966  ftc1a  25971  tdeglem4  25992  deg1pwle  26052  fta1blem  26103  aalioulem3  26269  aaliou2b  26276  ulmbdd  26334  ulmdvlem1  26336  itgulm  26344  pserdvlem2  26365  abelthlem3  26370  abelthlem5  26372  abelthlem6  26373  abelthlem7  26375  tanregt0  26475  argimlt0  26549  logdivlti  26556  logcnlem3  26580  logcnlem4  26581  logtayl  26596  logtayl2  26598  cxple2  26633  cxpcn3lem  26684  cxpaddle  26689  rtprmirr  26697  isosctrlem1  26755  atantayl  26874  efrlim  26906  efrlimOLD  26907  dfef2  26908  o1cxp  26912  cxp2lim  26914  divsqrtsumo1  26921  amgmlem  26927  logdifbnd  26931  emcllem7  26939  harmonicbnd4  26948  fsumharmonic  26949  lgamgulmlem2  26967  lgamgulmlem3  26968  lgamucov  26975  lgamcvg2  26992  gamcvg2  26997  ftalem2  27011  basellem2  27019  basellem5  27022  basellem9  27026  vma1  27103  sqff1o  27119  fsumfldivdiaglem  27126  chtub  27150  fsumvma2  27152  chpchtsum  27157  chpub  27158  logfaclbnd  27160  logfacbnd3  27161  logfacrlim  27162  logexprlim  27163  bcmono  27215  bposlem2  27223  bposlem5  27226  bposlem6  27227  lgsne0  27273  lgsquadlem1  27318  lgsquadlem2  27319  2sqblem  27369  2sqmod  27374  chebbnd1lem1  27407  chtppilimlem1  27411  chtppilimlem2  27412  chpchtlim  27417  rplogsumlem1  27422  dchrvmasumiflem1  27439  dchrisum0flblem2  27447  dchrisum0fno1  27449  dchrisum0lem2a  27455  dchrisum0lem3  27457  dirith  27467  mulog2sumlem1  27472  mulog2sumlem2  27473  log2sumbnd  27482  selberglem2  27484  logdivbnd  27494  selberg3lem1  27495  selberg4lem1  27498  pntrsumbnd2  27505  pntrlog2bndlem1  27515  pntrlog2bndlem5  27519  pntrlog2bndlem6  27521  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem3  27530  pntlemb  27535  pntlemn  27538  pntlemr  27540  pntlemj  27541  pntlemf  27543  pntlemo  27545  ostth2lem3  27573  ostth3  27576  addsuniflem  27944  sltp1d  27958  negsid  27983  negsunif  27997  mulsuniflem  28088  precsexlem9  28153  n0sge0  28266  zscut  28331  halfcut  28378  addhalfcut  28379  pw2cut2  28382  footeq  28702  hlperpnel  28703  perpdragALT  28705  perpdrag  28706  colperp  28707  mideulem2  28712  opphllem  28713  opphllem3  28727  lmieu  28762  trgcopy  28782  sacgr  28809  acopyeu  28812  usgredgleordALT  29212  eucrctshift  30223  nvabs  30652  smcnlem  30677  ubthlem2  30851  minvecolem4  30860  htthlem  30897  normpyc  31126  nmophmi  32011  hstle  32210  hstles  32211  stlei  32220  f1rnen  32610  nnmulge  32722  fsumiunle  32812  sgnmulsgn  32825  wrdt2ind  32934  xrge0npcan  33001  gsumwrd2dccat  33047  trsp2cyc  33092  archirngz  33158  archiabllem1a  33160  archiabllem2a  33163  archiabllem2c  33164  elrgspnlem1  33209  elrgspn  33213  elrgspnsubrunlem2  33215  rprmasso  33490  q1pdir  33563  r1pquslmic  33571  mplvrpmga  33575  mplvrpmrhm  33577  drngdimgt0  33631  lbsdiflsp0  33639  fldextrspundgle  33691  fldext2rspun  33695  minplyirredlem  33723  madjusmdetlem2  33841  esumpinfval  34086  esumpinfsum  34090  esumpcvgval  34091  esum2d  34106  esumiun  34107  dya2icoseg  34290  omssubadd  34313  carsgsigalem  34328  carsggect  34331  carsgclctunlem3  34333  omsmeas  34336  eulerpartlems  34373  signsplypnf  34563  signsply0  34564  reprlt  34632  reprinfz1  34635  hgt750lemc  34660  hgt750lemf  34666  pthhashvtx  35172  resconn  35290  sinccvglem  35716  circum  35718  btwnxfr  36100  nn0prpwlem  36366  dnibndlem2  36523  unblimceq0  36551  irrdiff  37370  poimirlem7  37677  mblfinlem3  37709  mblfinlem4  37710  itg2addnclem3  37723  ftc1anc  37751  isbnd3  37834  cntotbnd  37846  bfp  37874  rrndstprj2  37881  1cvrjat  39584  3atlem1  39592  3atlem6  39597  llnmlplnN  39648  2llnjaN  39675  2lplnja  39728  dalem57  39838  dalawlem11  39990  dalawlem12  39991  lhp2lt  40110  lhpj1  40131  lhpm0atN  40138  4atexlemex2  40180  lautm  40203  cdleme17b  40396  cdleme20j  40427  cdleme30a  40487  cdlemg4c  40721  cdlemg17a  40770  cdlemg31c  40808  trljco  40849  cdlemk46  41057  dia2dimlem2  41174  cdlemm10N  41227  cdlemn10  41315  dihmeetlem1N  41399  dihglblem5apreN  41400  dihmeetlem15N  41430  mapdat  41776  lcmineqlem19  42150  lcmineqlem20  42151  aks4d1p1p5  42178  aks4d1p8d2  42188  aks4d1p8  42190  aks4d1p9  42191  hashscontpow  42225  dvdsexpnn  42436  mullt0b1d  42586  selvvvval  42688  evlselv  42690  mhphflem  42699  fltnlta  42766  3cubeslem1  42787  irrapxlem1  42925  irrapxlem4  42928  pell1qrgaplem  42976  pellfundglb  42988  rmspecfund  43012  monotoddzzfi  43045  rmynn  43059  jm2.24nn  43062  jm2.17c  43065  jm2.24  43066  acongeq  43086  jm2.20nn  43100  jm2.26lem3  43104  jm2.27a  43108  jm2.27c  43110  rmydioph  43117  jm3.1lem2  43121  frlmpwfi  43201  areaquad  43319  cantnf2  43428  rp-isfinite6  43621  frege129d  43866  leeq1d  44260  imo72b2lem0  44268  imo72b2  44275  cvgdvgrat  44416  radcnvrat  44417  hashnzfzclim  44425  isosctrlem1ALT  45036  cncmpmax  45139  iooabslt  45609  fmul01lt1lem2  45695  clim1fr1  45711  limcrecl  45739  climxrrelem  45857  liminflbuz2  45923  dvnprodlem1  46054  stoweidlem1  46109  stoweidlem11  46119  stoweidlem14  46122  stoweidlem24  46132  stoweidlem26  46134  wallispilem4  46176  wallispilem5  46177  stirlinglem1  46182  fourierdlem51  46265  fourierdlem65  46279  fouriersw  46339  2leaddle2  47408  sqrtpwpw2p  47648  lighneallem4a  47718  flnn0div2ge  48644  logbpw2m1  48678  functermclem  49618  amgmwlem  49913