Theorem eqbrtrrd 5173

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 5171	1 ⊢ (𝜑 → 𝐵𝑅𝐶)

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

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  dftpos4  8230  dif1en  9160  dif1enOLD  9162  fodomfi  9325  fmptssfisupp  9389  resfifsupp  9392  cnfcom2lem  9696  dmttrcl  9716  ttrclselem2  9721  ficardadju  10194  enfin1ai  10379  pwcfsdom  10578  fpwwe2lem6  10631  fpwwe2  10638  canthp1lem1  10647  1nqenq  10957  prlem936  11042  lemulge11  12076  supaddc  12181  supmul1  12183  mul2lt0llt0  13078  mul2lt0lgt0  13079  xaddge0  13237  xadddi2  13276  ltexp2a  14131  leexp2a  14137  nnlesq  14169  digit1  14200  faclbnd4lem1  14253  faclbnd6  14259  facavg  14261  prsshashgt1  14370  nehash2  14435  abs3dif  15278  abs2dif  15279  limsupgre  15425  rlimclim1  15489  rlimuni  15494  rlimres2  15505  rlimcn1  15532  rlimcn1b  15533  recn2  15545  imcn2  15546  rlimo1  15561  o1rlimmul  15563  iserex  15603  isercoll  15614  caucvgrlem2  15621  caucvgr  15622  iseraltlem3  15630  summolem2a  15661  fsumge1  15743  o1fsum  15759  isumrpcl  15789  climcnds  15797  harmonic  15805  mertenslem1  15830  prodmolem2a  15878  ege2le3  16033  efgt1p2  16057  efgt1p  16058  eirrlem  16147  rpnnen2lem11  16167  fsumdvds  16251  bitsfzo  16376  bitsmod  16377  bitscmp  16379  mulgcd  16490  dvdssqlem  16503  nn0seqcvgd  16507  mulgcddvds  16592  rpdvds  16597  qden1elz  16693  phimullem  16712  hashgcdlem  16721  hashgcdeq  16722  pcdvdstr  16809  pockthg  16839  prmreclem1  16849  4sqlem11  16888  ramub1lem1  16959  ramub1lem2  16960  mreexexlem4d  17591  sscid  17771  latmlej21  18433  latmlej22  18434  lubel  18467  efginvrel1  19596  odadd2  19717  odadd  19718  gexexlem  19720  cyggex2  19765  ablfacrplem  19935  ablfac1c  19941  ablfac1eu  19943  pgpfac1lem3a  19946  isabvd  20428  mptscmfsuppd  20538  znrrg  21121  frlmphl  21336  frlmup1  21353  f1linds  21380  chcoeffeqlem  22387  lmcn2  23153  metrtri  23863  imasdsf1olem  23879  stdbdxmet  24024  nrmmetd  24083  nmmtri  24131  nlmvscnlem2  24202  blcvx  24314  recld2  24330  zdis  24332  opnreen  24347  cnheibor  24471  lebnumlem3  24479  nmoleub2lem3  24631  nmoleub2lem2  24632  nmoleub3  24635  ipcnlem2  24761  cmetcaulem  24805  nglmle  24819  cncmet  24839  csbren  24916  trirn  24917  minveclem4  24949  ovoliunlem1  25019  ovoliun2  25023  ovolscalem1  25030  ovolicopnf  25041  voliunlem2  25068  volsup  25073  ioorcl2  25089  uniiccvol  25097  uniioombllem4  25103  i1fd  25198  mbfi1fseqlem4  25236  itg2const2  25259  itg2eqa  25263  itg2split  25267  itg2i1fseqle  25272  itg2cnlem2  25280  dvcnv  25494  dveflem  25496  dvferm1lem  25501  dvlip2  25512  c1liplem1  25513  dvivthlem1  25525  lhop1lem  25530  dvcvx  25537  dvfsumle  25538  dvfsumabs  25540  dvfsumlem4  25546  dvfsumrlim2  25549  ftc1a  25554  tdeglem4  25577  tdeglem4OLD  25578  deg1pwle  25637  fta1blem  25686  aalioulem3  25847  aaliou2b  25854  ulmbdd  25910  ulmdvlem1  25912  itgulm  25920  pserdvlem2  25940  abelthlem3  25945  abelthlem5  25947  abelthlem6  25948  abelthlem7  25950  tanregt0  26048  argimlt0  26121  logdivlti  26128  logcnlem3  26152  logcnlem4  26153  logtayl  26168  logtayl2  26170  cxple2  26205  cxpcn3lem  26255  cxpaddle  26260  isosctrlem1  26323  atantayl  26442  efrlim  26474  dfef2  26475  o1cxp  26479  cxp2lim  26481  divsqrtsumo1  26488  amgmlem  26494  logdifbnd  26498  emcllem7  26506  harmonicbnd4  26515  fsumharmonic  26516  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamucov  26542  lgamcvg2  26559  gamcvg2  26564  ftalem2  26578  basellem2  26586  basellem5  26589  basellem9  26593  vma1  26670  sqff1o  26686  fsumfldivdiaglem  26693  chtub  26715  fsumvma2  26717  chpchtsum  26722  chpub  26723  logfaclbnd  26725  logfacbnd3  26726  logfacrlim  26727  logexprlim  26728  bcmono  26780  bposlem2  26788  bposlem5  26791  bposlem6  26792  lgsne0  26838  lgsquadlem1  26883  lgsquadlem2  26884  2sqblem  26934  2sqmod  26939  chebbnd1lem1  26972  chtppilimlem1  26976  chtppilimlem2  26977  chpchtlim  26982  rplogsumlem1  26987  dchrvmasumiflem1  27004  dchrisum0flblem2  27012  dchrisum0fno1  27014  dchrisum0lem2a  27020  dchrisum0lem3  27022  dirith  27032  mulog2sumlem1  27037  mulog2sumlem2  27038  log2sumbnd  27047  selberglem2  27049  logdivbnd  27059  selberg3lem1  27060  selberg4lem1  27063  pntrsumbnd2  27070  pntrlog2bndlem1  27080  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntpbnd1a  27088  pntpbnd1  27089  pntpbnd2  27090  pntibndlem3  27095  pntlemb  27100  pntlemn  27103  pntlemr  27105  pntlemj  27106  pntlemf  27108  pntlemo  27110  ostth2lem3  27138  ostth3  27141  addsuniflem  27484  negsid  27515  negsunif  27529  mulsuniflem  27604  precsexlem9  27661  footeq  27975  hlperpnel  27976  perpdragALT  27978  perpdrag  27979  colperp  27980  mideulem2  27985  opphllem  27986  opphllem3  28000  lmieu  28035  trgcopy  28055  sacgr  28082  acopyeu  28085  usgredgleordALT  28491  eucrctshift  29496  nvabs  29925  smcnlem  29950  ubthlem2  30124  minvecolem4  30133  htthlem  30170  normpyc  30399  nmophmi  31284  hstle  31483  hstles  31484  stlei  31493  f1rnen  31853  nnmulge  31963  fsumiunle  32035  wrdt2ind  32117  xrge0npcan  32195  trsp2cyc  32282  archirngz  32335  archiabllem1a  32337  archiabllem2a  32340  archiabllem2c  32341  ornglmulle  32423  orngrmulle  32424  drngdimgt0  32703  lbsdiflsp0  32711  minplyirredlem  32769  madjusmdetlem2  32808  esumpinfval  33071  esumpinfsum  33075  esumpcvgval  33076  esum2d  33091  esumiun  33092  dya2icoseg  33276  omssubadd  33299  carsgsigalem  33314  carsggect  33317  carsgclctunlem3  33319  omsmeas  33322  eulerpartlems  33359  sgnmulsgn  33548  signsplypnf  33561  signsply0  33562  reprlt  33631  reprinfz1  33634  hgt750lemc  33659  hgt750lemf  33665  pthhashvtx  34118  resconn  34237  sinccvglem  34657  circum  34659  btwnxfr  35028  gg-dvfsumle  35182  nn0prpwlem  35207  dnibndlem2  35355  unblimceq0  35383  irrdiff  36207  poimirlem7  36495  mblfinlem3  36527  mblfinlem4  36528  itg2addnclem3  36541  ftc1anc  36569  isbnd3  36652  cntotbnd  36664  bfp  36692  rrndstprj2  36699  1cvrjat  38346  3atlem1  38354  3atlem6  38359  llnmlplnN  38410  2llnjaN  38437  2lplnja  38490  dalem57  38600  dalawlem11  38752  dalawlem12  38753  lhp2lt  38872  lhpj1  38893  lhpm0atN  38900  4atexlemex2  38942  lautm  38965  cdleme17b  39158  cdleme20j  39189  cdleme30a  39249  cdlemg4c  39483  cdlemg17a  39532  cdlemg31c  39570  trljco  39611  cdlemk46  39819  dia2dimlem2  39936  cdlemm10N  39989  cdlemn10  40077  dihmeetlem1N  40161  dihglblem5apreN  40162  dihmeetlem15N  40192  mapdat  40538  lcmineqlem19  40912  lcmineqlem20  40913  aks4d1p1p5  40940  aks4d1p8d2  40950  aks4d1p8  40952  aks4d1p9  40953  metakunt29  41013  2xp3dxp2ge1d  41022  factwoffsmonot  41023  selvvvval  41157  evlselv  41159  mhphflem  41168  dvdsexpnn  41231  rtprmirr  41237  fltnlta  41405  3cubeslem1  41422  irrapxlem1  41560  irrapxlem4  41563  pell1qrgaplem  41611  pellfundglb  41623  rmspecfund  41647  monotoddzzfi  41681  rmynn  41695  jm2.24nn  41698  jm2.17c  41701  jm2.24  41702  acongeq  41722  jm2.20nn  41736  jm2.26lem3  41740  jm2.27a  41744  jm2.27c  41746  rmydioph  41753  jm3.1lem2  41757  frlmpwfi  41840  areaquad  41965  cantnf2  42075  rp-isfinite6  42269  frege129d  42514  leeq1d  42908  imo72b2  42924  cvgdvgrat  43072  radcnvrat  43073  hashnzfzclim  43081  isosctrlem1ALT  43695  cncmpmax  43716  iooabslt  44212  fmul01lt1lem2  44301  clim1fr1  44317  limcrecl  44345  climxrrelem  44465  liminflbuz2  44531  stoweidlem1  44717  stoweidlem11  44727  stoweidlem14  44730  stoweidlem24  44740  stoweidlem26  44742  wallispilem4  44784  wallispilem5  44785  stirlinglem1  44790  fourierdlem51  44873  fourierdlem65  44887  fouriersw  44947  2leaddle2  46006  sqrtpwpw2p  46206  lighneallem4a  46276  flnn0div2ge  47219  logbpw2m1  47253  amgmwlem  47849