Theorem eqbrtrrd 5126

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  dftpos4  8201  dif1en  9101  dif1enOLD  9103  fodomfi  9237  fodomfiOLD  9257  fmptssfisupp  9321  resfifsupp  9324  cnfcom2lem  9630  dmttrcl  9650  ttrclselem2  9655  ficardadju  10129  enfin1ai  10313  pwcfsdom  10512  fpwwe2lem6  10565  fpwwe2  10572  canthp1lem1  10581  1nqenq  10891  prlem936  10976  lemulge11  12021  supaddc  12126  supmul1  12128  mul2lt0llt0  13033  mul2lt0lgt0  13034  xaddge0  13194  xadddi2  13233  ltexp2a  14107  leexp2a  14113  nnlesq  14146  digit1  14178  faclbnd4lem1  14234  faclbnd6  14240  facavg  14242  prsshashgt1  14351  nehash2  14415  abs3dif  15274  abs2dif  15275  limsupgre  15423  rlimclim1  15487  rlimuni  15492  rlimres2  15503  rlimcn1  15530  rlimcn1b  15531  recn2  15543  imcn2  15544  rlimo1  15559  o1rlimmul  15561  iserex  15599  isercoll  15610  caucvgrlem2  15617  caucvgr  15618  iseraltlem3  15626  summolem2a  15657  fsumge1  15739  o1fsum  15755  isumrpcl  15785  climcnds  15793  harmonic  15801  mertenslem1  15826  prodmolem2a  15876  ege2le3  16032  efgt1p2  16058  efgt1p  16059  eirrlem  16148  rpnnen2lem11  16168  fsumdvds  16254  bitsfzo  16381  bitsmod  16382  bitscmp  16384  mulgcd  16494  dvdssqlem  16512  nn0seqcvgd  16516  mulgcddvds  16601  rpdvds  16606  qden1elz  16703  phimullem  16725  hashgcdlem  16734  hashgcdeq  16736  pcdvdstr  16823  pockthg  16853  prmreclem1  16863  4sqlem11  16902  ramub1lem1  16973  ramub1lem2  16974  mreexexlem4d  17584  sscid  17762  latmlej21  18415  latmlej22  18416  lubel  18449  efginvrel1  19634  odadd2  19755  odadd  19756  gexexlem  19758  cyggex2  19803  ablfacrplem  19973  ablfac1c  19979  ablfac1eu  19981  pgpfac1lem3a  19984  isabvd  20697  mptscmfsuppd  20810  znrrg  21451  frlmphl  21666  frlmup1  21683  f1linds  21710  psdmplcl  22025  chcoeffeqlem  22748  lmcn2  23512  metrtri  24221  imasdsf1olem  24237  stdbdxmet  24379  nrmmetd  24438  nmmtri  24486  nlmvscnlem2  24549  blcvx  24662  recld2  24679  zdis  24681  opnreen  24696  cnheibor  24830  lebnumlem3  24838  nmoleub2lem3  24991  nmoleub2lem2  24992  nmoleub3  24995  ipcnlem2  25120  cmetcaulem  25164  nglmle  25178  cncmet  25198  csbren  25275  trirn  25276  minveclem4  25308  ovoliunlem1  25379  ovoliun2  25383  ovolscalem1  25390  ovolicopnf  25401  voliunlem2  25428  volsup  25433  ioorcl2  25449  uniiccvol  25457  uniioombllem4  25463  i1fd  25558  mbfi1fseqlem4  25595  itg2const2  25618  itg2eqa  25622  itg2split  25626  itg2i1fseqle  25631  itg2cnlem2  25639  dvcnv  25857  dveflem  25859  dvferm1lem  25864  dvlip2  25876  c1liplem1  25877  dvivthlem1  25889  lhop1lem  25894  dvcvx  25901  dvfsumle  25902  dvfsumleOLD  25903  dvfsumabs  25905  dvfsumlem4  25912  dvfsumrlim2  25915  ftc1a  25920  tdeglem4  25941  deg1pwle  26001  fta1blem  26052  aalioulem3  26218  aaliou2b  26225  ulmbdd  26283  ulmdvlem1  26285  itgulm  26293  pserdvlem2  26314  abelthlem3  26319  abelthlem5  26321  abelthlem6  26322  abelthlem7  26324  tanregt0  26424  argimlt0  26498  logdivlti  26505  logcnlem3  26529  logcnlem4  26530  logtayl  26545  logtayl2  26547  cxple2  26582  cxpcn3lem  26633  cxpaddle  26638  rtprmirr  26646  isosctrlem1  26704  atantayl  26823  efrlim  26855  efrlimOLD  26856  dfef2  26857  o1cxp  26861  cxp2lim  26863  divsqrtsumo1  26870  amgmlem  26876  logdifbnd  26880  emcllem7  26888  harmonicbnd4  26897  fsumharmonic  26898  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamucov  26924  lgamcvg2  26941  gamcvg2  26946  ftalem2  26960  basellem2  26968  basellem5  26971  basellem9  26975  vma1  27052  sqff1o  27068  fsumfldivdiaglem  27075  chtub  27099  fsumvma2  27101  chpchtsum  27106  chpub  27107  logfaclbnd  27109  logfacbnd3  27110  logfacrlim  27111  logexprlim  27112  bcmono  27164  bposlem2  27172  bposlem5  27175  bposlem6  27176  lgsne0  27222  lgsquadlem1  27267  lgsquadlem2  27268  2sqblem  27318  2sqmod  27323  chebbnd1lem1  27356  chtppilimlem1  27360  chtppilimlem2  27361  chpchtlim  27366  rplogsumlem1  27371  dchrvmasumiflem1  27388  dchrisum0flblem2  27396  dchrisum0fno1  27398  dchrisum0lem2a  27404  dchrisum0lem3  27406  dirith  27416  mulog2sumlem1  27421  mulog2sumlem2  27422  log2sumbnd  27431  selberglem2  27433  logdivbnd  27443  selberg3lem1  27444  selberg4lem1  27447  pntrsumbnd2  27454  pntrlog2bndlem1  27464  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntpbnd1a  27472  pntpbnd1  27473  pntpbnd2  27474  pntibndlem3  27479  pntlemb  27484  pntlemn  27487  pntlemr  27489  pntlemj  27490  pntlemf  27492  pntlemo  27494  ostth2lem3  27522  ostth3  27525  addsuniflem  27884  sltp1d  27898  negsid  27923  negsunif  27937  mulsuniflem  28028  precsexlem9  28093  n0sge0  28206  zscut  28271  halfcut  28309  addhalfcut  28310  footeq  28627  hlperpnel  28628  perpdragALT  28630  perpdrag  28631  colperp  28632  mideulem2  28637  opphllem  28638  opphllem3  28652  lmieu  28687  trgcopy  28707  sacgr  28734  acopyeu  28737  usgredgleordALT  29137  eucrctshift  30145  nvabs  30574  smcnlem  30599  ubthlem2  30773  minvecolem4  30782  htthlem  30819  normpyc  31048  nmophmi  31933  hstle  32132  hstles  32133  stlei  32142  f1rnen  32526  nnmulge  32635  fsumiunle  32727  sgnmulsgn  32740  wrdt2ind  32848  xrge0npcan  32934  gsumwrd2dccat  32980  trsp2cyc  33053  archirngz  33116  archiabllem1a  33118  archiabllem2a  33121  archiabllem2c  33122  elrgspnlem1  33166  elrgspn  33170  elrgspnsubrunlem2  33172  ornglmulle  33256  orngrmulle  33257  rprmasso  33469  q1pdir  33541  r1pquslmic  33549  drngdimgt0  33587  lbsdiflsp0  33595  fldextrspundgle  33646  fldext2rspun  33650  minplyirredlem  33673  madjusmdetlem2  33791  esumpinfval  34036  esumpinfsum  34040  esumpcvgval  34041  esum2d  34056  esumiun  34057  dya2icoseg  34241  omssubadd  34264  carsgsigalem  34279  carsggect  34282  carsgclctunlem3  34284  omsmeas  34287  eulerpartlems  34324  signsplypnf  34514  signsply0  34515  reprlt  34583  reprinfz1  34586  hgt750lemc  34611  hgt750lemf  34617  pthhashvtx  35088  resconn  35206  sinccvglem  35632  circum  35634  btwnxfr  36017  nn0prpwlem  36283  dnibndlem2  36440  unblimceq0  36468  irrdiff  37287  poimirlem7  37594  mblfinlem3  37626  mblfinlem4  37627  itg2addnclem3  37640  ftc1anc  37668  isbnd3  37751  cntotbnd  37763  bfp  37791  rrndstprj2  37798  1cvrjat  39442  3atlem1  39450  3atlem6  39455  llnmlplnN  39506  2llnjaN  39533  2lplnja  39586  dalem57  39696  dalawlem11  39848  dalawlem12  39849  lhp2lt  39968  lhpj1  39989  lhpm0atN  39996  4atexlemex2  40038  lautm  40061  cdleme17b  40254  cdleme20j  40285  cdleme30a  40345  cdlemg4c  40579  cdlemg17a  40628  cdlemg31c  40666  trljco  40707  cdlemk46  40915  dia2dimlem2  41032  cdlemm10N  41085  cdlemn10  41173  dihmeetlem1N  41257  dihglblem5apreN  41258  dihmeetlem15N  41288  mapdat  41634  lcmineqlem19  42008  lcmineqlem20  42009  aks4d1p1p5  42036  aks4d1p8d2  42046  aks4d1p8  42048  aks4d1p9  42049  hashscontpow  42083  dvdsexpnn  42294  mullt0b1d  42444  selvvvval  42546  evlselv  42548  mhphflem  42557  fltnlta  42624  3cubeslem1  42645  irrapxlem1  42783  irrapxlem4  42786  pell1qrgaplem  42834  pellfundglb  42846  rmspecfund  42870  monotoddzzfi  42904  rmynn  42918  jm2.24nn  42921  jm2.17c  42924  jm2.24  42925  acongeq  42945  jm2.20nn  42959  jm2.26lem3  42963  jm2.27a  42967  jm2.27c  42969  rmydioph  42976  jm3.1lem2  42980  frlmpwfi  43060  areaquad  43178  cantnf2  43287  rp-isfinite6  43480  frege129d  43725  leeq1d  44119  imo72b2lem0  44127  imo72b2  44134  cvgdvgrat  44275  radcnvrat  44276  hashnzfzclim  44284  isosctrlem1ALT  44896  cncmpmax  44999  iooabslt  45470  fmul01lt1lem2  45556  clim1fr1  45572  limcrecl  45600  climxrrelem  45720  liminflbuz2  45786  dvnprodlem1  45917  stoweidlem1  45972  stoweidlem11  45982  stoweidlem14  45985  stoweidlem24  45995  stoweidlem26  45997  wallispilem4  46039  wallispilem5  46040  stirlinglem1  46045  fourierdlem51  46128  fourierdlem65  46142  fouriersw  46202  2leaddle2  47272  sqrtpwpw2p  47512  lighneallem4a  47582  flnn0div2ge  48495  logbpw2m1  48529  functermclem  49469  amgmwlem  49764