Theorem eqbrtrrd 5172

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5148

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  dftpos4  8227  dif1en  9157  dif1enOLD  9159  fodomfi  9322  fmptssfisupp  9386  resfifsupp  9389  cnfcom2lem  9693  dmttrcl  9713  ttrclselem2  9718  ficardadju  10191  enfin1ai  10376  pwcfsdom  10575  fpwwe2lem6  10628  fpwwe2  10635  canthp1lem1  10644  1nqenq  10954  prlem936  11039  lemulge11  12073  supaddc  12178  supmul1  12180  mul2lt0llt0  13075  mul2lt0lgt0  13076  xaddge0  13234  xadddi2  13273  ltexp2a  14128  leexp2a  14134  nnlesq  14166  digit1  14197  faclbnd4lem1  14250  faclbnd6  14256  facavg  14258  prsshashgt1  14367  nehash2  14432  abs3dif  15275  abs2dif  15276  limsupgre  15422  rlimclim1  15486  rlimuni  15491  rlimres2  15502  rlimcn1  15529  rlimcn1b  15530  recn2  15542  imcn2  15543  rlimo1  15558  o1rlimmul  15560  iserex  15600  isercoll  15611  caucvgrlem2  15618  caucvgr  15619  iseraltlem3  15627  summolem2a  15658  fsumge1  15740  o1fsum  15756  isumrpcl  15786  climcnds  15794  harmonic  15802  mertenslem1  15827  prodmolem2a  15875  ege2le3  16030  efgt1p2  16054  efgt1p  16055  eirrlem  16144  rpnnen2lem11  16164  fsumdvds  16248  bitsfzo  16373  bitsmod  16374  bitscmp  16376  mulgcd  16487  dvdssqlem  16500  nn0seqcvgd  16504  mulgcddvds  16589  rpdvds  16594  qden1elz  16690  phimullem  16709  hashgcdlem  16718  hashgcdeq  16719  pcdvdstr  16806  pockthg  16836  prmreclem1  16846  4sqlem11  16885  ramub1lem1  16956  ramub1lem2  16957  mreexexlem4d  17588  sscid  17768  latmlej21  18430  latmlej22  18431  lubel  18464  efginvrel1  19591  odadd2  19712  odadd  19713  gexexlem  19715  cyggex2  19760  ablfacrplem  19930  ablfac1c  19936  ablfac1eu  19938  pgpfac1lem3a  19941  isabvd  20421  mptscmfsuppd  20531  znrrg  21113  frlmphl  21328  frlmup1  21345  f1linds  21372  chcoeffeqlem  22379  lmcn2  23145  metrtri  23855  imasdsf1olem  23871  stdbdxmet  24016  nrmmetd  24075  nmmtri  24123  nlmvscnlem2  24194  blcvx  24306  recld2  24322  zdis  24324  opnreen  24339  cnheibor  24463  lebnumlem3  24471  nmoleub2lem3  24623  nmoleub2lem2  24624  nmoleub3  24627  ipcnlem2  24753  cmetcaulem  24797  nglmle  24811  cncmet  24831  csbren  24908  trirn  24909  minveclem4  24941  ovoliunlem1  25011  ovoliun2  25015  ovolscalem1  25022  ovolicopnf  25033  voliunlem2  25060  volsup  25065  ioorcl2  25081  uniiccvol  25089  uniioombllem4  25095  i1fd  25190  mbfi1fseqlem4  25228  itg2const2  25251  itg2eqa  25255  itg2split  25259  itg2i1fseqle  25264  itg2cnlem2  25272  dvcnv  25486  dveflem  25488  dvferm1lem  25493  dvlip2  25504  c1liplem1  25505  dvivthlem1  25517  lhop1lem  25522  dvcvx  25529  dvfsumle  25530  dvfsumabs  25532  dvfsumlem4  25538  dvfsumrlim2  25541  ftc1a  25546  tdeglem4  25569  tdeglem4OLD  25570  deg1pwle  25629  fta1blem  25678  aalioulem3  25839  aaliou2b  25846  ulmbdd  25902  ulmdvlem1  25904  itgulm  25912  pserdvlem2  25932  abelthlem3  25937  abelthlem5  25939  abelthlem6  25940  abelthlem7  25942  tanregt0  26040  argimlt0  26113  logdivlti  26120  logcnlem3  26144  logcnlem4  26145  logtayl  26160  logtayl2  26162  cxple2  26197  cxpcn3lem  26245  cxpaddle  26250  isosctrlem1  26313  atantayl  26432  efrlim  26464  dfef2  26465  o1cxp  26469  cxp2lim  26471  divsqrtsumo1  26478  amgmlem  26484  logdifbnd  26488  emcllem7  26496  harmonicbnd4  26505  fsumharmonic  26506  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamucov  26532  lgamcvg2  26549  gamcvg2  26554  ftalem2  26568  basellem2  26576  basellem5  26579  basellem9  26583  vma1  26660  sqff1o  26676  fsumfldivdiaglem  26683  chtub  26705  fsumvma2  26707  chpchtsum  26712  chpub  26713  logfaclbnd  26715  logfacbnd3  26716  logfacrlim  26717  logexprlim  26718  bcmono  26770  bposlem2  26778  bposlem5  26781  bposlem6  26782  lgsne0  26828  lgsquadlem1  26873  lgsquadlem2  26874  2sqblem  26924  2sqmod  26929  chebbnd1lem1  26962  chtppilimlem1  26966  chtppilimlem2  26967  chpchtlim  26972  rplogsumlem1  26977  dchrvmasumiflem1  26994  dchrisum0flblem2  27002  dchrisum0fno1  27004  dchrisum0lem2a  27010  dchrisum0lem3  27012  dirith  27022  mulog2sumlem1  27027  mulog2sumlem2  27028  log2sumbnd  27037  selberglem2  27039  logdivbnd  27049  selberg3lem1  27050  selberg4lem1  27053  pntrsumbnd2  27060  pntrlog2bndlem1  27070  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  pntibndlem3  27085  pntlemb  27090  pntlemn  27093  pntlemr  27095  pntlemj  27096  pntlemf  27098  pntlemo  27100  ostth2lem3  27128  ostth3  27131  addsuniflem  27474  negsid  27505  negsunif  27519  mulsuniflem  27594  precsexlem9  27651  footeq  27965  hlperpnel  27966  perpdragALT  27968  perpdrag  27969  colperp  27970  mideulem2  27975  opphllem  27976  opphllem3  27990  lmieu  28025  trgcopy  28045  sacgr  28072  acopyeu  28075  usgredgleordALT  28481  eucrctshift  29486  nvabs  29913  smcnlem  29938  ubthlem2  30112  minvecolem4  30121  htthlem  30158  normpyc  30387  nmophmi  31272  hstle  31471  hstles  31472  stlei  31481  f1rnen  31841  nnmulge  31951  fsumiunle  32023  wrdt2ind  32105  xrge0npcan  32183  trsp2cyc  32270  archirngz  32323  archiabllem1a  32325  archiabllem2a  32328  archiabllem2c  32329  ornglmulle  32412  orngrmulle  32413  drngdimgt0  32692  lbsdiflsp0  32700  minplyirredlem  32758  madjusmdetlem2  32797  esumpinfval  33060  esumpinfsum  33064  esumpcvgval  33065  esum2d  33080  esumiun  33081  dya2icoseg  33265  omssubadd  33288  carsgsigalem  33303  carsggect  33306  carsgclctunlem3  33308  omsmeas  33311  eulerpartlems  33348  sgnmulsgn  33537  signsplypnf  33550  signsply0  33551  reprlt  33620  reprinfz1  33623  hgt750lemc  33648  hgt750lemf  33654  pthhashvtx  34107  resconn  34226  sinccvglem  34646  circum  34648  btwnxfr  35017  gg-dvfsumle  35171  nn0prpwlem  35196  dnibndlem2  35344  unblimceq0  35372  irrdiff  36196  poimirlem7  36484  mblfinlem3  36516  mblfinlem4  36517  itg2addnclem3  36530  ftc1anc  36558  isbnd3  36641  cntotbnd  36653  bfp  36681  rrndstprj2  36688  1cvrjat  38335  3atlem1  38343  3atlem6  38348  llnmlplnN  38399  2llnjaN  38426  2lplnja  38479  dalem57  38589  dalawlem11  38741  dalawlem12  38742  lhp2lt  38861  lhpj1  38882  lhpm0atN  38889  4atexlemex2  38931  lautm  38954  cdleme17b  39147  cdleme20j  39178  cdleme30a  39238  cdlemg4c  39472  cdlemg17a  39521  cdlemg31c  39559  trljco  39600  cdlemk46  39808  dia2dimlem2  39925  cdlemm10N  39978  cdlemn10  40066  dihmeetlem1N  40150  dihglblem5apreN  40151  dihmeetlem15N  40181  mapdat  40527  lcmineqlem19  40901  lcmineqlem20  40902  aks4d1p1p5  40929  aks4d1p8d2  40939  aks4d1p8  40941  aks4d1p9  40942  metakunt29  41002  2xp3dxp2ge1d  41011  factwoffsmonot  41012  selvvvval  41155  evlselv  41157  mhphflem  41166  dvdsexpnn  41227  rtprmirr  41234  fltnlta  41402  3cubeslem1  41408  irrapxlem1  41546  irrapxlem4  41549  pell1qrgaplem  41597  pellfundglb  41609  rmspecfund  41633  monotoddzzfi  41667  rmynn  41681  jm2.24nn  41684  jm2.17c  41687  jm2.24  41688  acongeq  41708  jm2.20nn  41722  jm2.26lem3  41726  jm2.27a  41730  jm2.27c  41732  rmydioph  41739  jm3.1lem2  41743  frlmpwfi  41826  areaquad  41951  cantnf2  42061  rp-isfinite6  42255  frege129d  42500  leeq1d  42894  imo72b2  42910  cvgdvgrat  43058  radcnvrat  43059  hashnzfzclim  43067  isosctrlem1ALT  43681  cncmpmax  43702  iooabslt  44199  fmul01lt1lem2  44288  clim1fr1  44304  limcrecl  44332  climxrrelem  44452  liminflbuz2  44518  stoweidlem1  44704  stoweidlem11  44714  stoweidlem14  44717  stoweidlem24  44727  stoweidlem26  44729  wallispilem4  44771  wallispilem5  44772  stirlinglem1  44777  fourierdlem51  44860  fourierdlem65  44874  fouriersw  44934  2leaddle2  45993  sqrtpwpw2p  46193  lighneallem4a  46263  flnn0div2ge  47173  logbpw2m1  47207  amgmwlem  47803