Theorem eqbrtrrd 5054

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  dftpos4  7894  fodomfi  8781  resfifsupp  8845  cnfcom2lem  9148  ficardadju  9610  enfin1ai  9795  pwcfsdom  9994  fpwwe2lem7  10047  fpwwe2  10054  canthp1lem1  10063  1nqenq  10373  prlem936  10458  lemulge11  11491  supaddc  11595  supmul1  11597  mul2lt0llt0  12481  mul2lt0lgt0  12482  xaddge0  12639  xadddi2  12678  ltexp2a  13526  leexp2a  13532  nnlesq  13564  digit1  13594  faclbnd4lem1  13649  faclbnd6  13655  facavg  13657  prsshashgt1  13767  nehash2  13828  abs3dif  14683  abs2dif  14684  limsupgre  14830  rlimclim1  14894  rlimuni  14899  rlimres2  14910  rlimcn1  14937  rlimcn1b  14938  recn2  14949  imcn2  14950  rlimo1  14965  o1rlimmul  14967  iserex  15005  isercoll  15016  caucvgrlem2  15023  caucvgr  15024  iseraltlem3  15032  summolem2a  15064  fsumge1  15144  o1fsum  15160  isumrpcl  15190  climcnds  15198  harmonic  15206  mertenslem1  15232  prodmolem2a  15280  ege2le3  15435  efgt1p2  15459  efgt1p  15460  eirrlem  15549  rpnnen2lem11  15569  fsumdvds  15650  bitsfzo  15774  bitsmod  15775  bitscmp  15777  mulgcd  15886  dvdssqlem  15900  nn0seqcvgd  15904  mulgcddvds  15989  rpdvds  15994  qden1elz  16087  phimullem  16106  hashgcdlem  16115  hashgcdeq  16116  pcdvdstr  16202  pockthg  16232  prmreclem1  16242  4sqlem11  16281  ramub1lem1  16352  ramub1lem2  16353  mreexexlem4d  16910  sscid  17086  latmlej21  17694  latmlej22  17695  lubel  17724  efginvrel1  18846  odadd2  18962  odadd  18963  gexexlem  18965  cyggex2  19010  ablfacrplem  19180  ablfac1c  19186  ablfac1eu  19188  pgpfac1lem3a  19191  isabvd  19584  mptscmfsuppd  19693  znrrg  20257  frlmphl  20470  frlmup1  20487  f1linds  20514  chcoeffeqlem  21490  lmcn2  22254  metrtri  22964  imasdsf1olem  22980  stdbdxmet  23122  nrmmetd  23181  nmmtri  23228  nlmvscnlem2  23291  blcvx  23403  recld2  23419  zdis  23421  opnreen  23436  cnheibor  23560  lebnumlem3  23568  nmoleub2lem3  23720  nmoleub2lem2  23721  nmoleub3  23724  ipcnlem2  23848  cmetcaulem  23892  nglmle  23906  cncmet  23926  csbren  24003  trirn  24004  minveclem4  24036  ovoliunlem1  24106  ovoliun2  24110  ovolscalem1  24117  ovolicopnf  24128  voliunlem2  24155  volsup  24160  ioorcl2  24176  uniiccvol  24184  uniioombllem4  24190  i1fd  24285  mbfi1fseqlem4  24322  itg2const2  24345  itg2eqa  24349  itg2split  24353  itg2i1fseqle  24358  itg2cnlem2  24366  dvcnv  24580  dveflem  24582  dvferm1lem  24587  dvlip2  24598  c1liplem1  24599  dvivthlem1  24611  lhop1lem  24616  dvcvx  24623  dvfsumle  24624  dvfsumabs  24626  dvfsumlem4  24632  dvfsumrlim2  24635  ftc1a  24640  tdeglem4  24661  deg1pwle  24720  fta1blem  24769  aalioulem3  24930  aaliou2b  24937  ulmbdd  24993  ulmdvlem1  24995  itgulm  25003  pserdvlem2  25023  abelthlem3  25028  abelthlem5  25030  abelthlem6  25031  abelthlem7  25033  tanregt0  25131  argimlt0  25204  logdivlti  25211  logcnlem3  25235  logcnlem4  25236  logtayl  25251  logtayl2  25253  cxple2  25288  cxpcn3lem  25336  cxpaddle  25341  isosctrlem1  25404  atantayl  25523  efrlim  25555  dfef2  25556  o1cxp  25560  cxp2lim  25562  divsqrtsumo1  25569  amgmlem  25575  logdifbnd  25579  emcllem7  25587  harmonicbnd4  25596  fsumharmonic  25597  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamucov  25623  lgamcvg2  25640  gamcvg2  25645  ftalem2  25659  basellem2  25667  basellem5  25670  basellem9  25674  vma1  25751  sqff1o  25767  fsumfldivdiaglem  25774  chtub  25796  fsumvma2  25798  chpchtsum  25803  chpub  25804  logfaclbnd  25806  logfacbnd3  25807  logfacrlim  25808  logexprlim  25809  bcmono  25861  bposlem2  25869  bposlem5  25872  bposlem6  25873  lgsne0  25919  lgsquadlem1  25964  lgsquadlem2  25965  2sqblem  26015  2sqmod  26020  chebbnd1lem1  26053  chtppilimlem1  26057  chtppilimlem2  26058  chpchtlim  26063  rplogsumlem1  26068  dchrvmasumiflem1  26085  dchrisum0flblem2  26093  dchrisum0fno1  26095  dchrisum0lem2a  26101  dchrisum0lem3  26103  dirith  26113  mulog2sumlem1  26118  mulog2sumlem2  26119  log2sumbnd  26128  selberglem2  26130  logdivbnd  26140  selberg3lem1  26141  selberg4lem1  26144  pntrsumbnd2  26151  pntrlog2bndlem1  26161  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntpbnd1a  26169  pntpbnd1  26170  pntpbnd2  26171  pntibndlem3  26176  pntlemb  26181  pntlemn  26184  pntlemr  26186  pntlemj  26187  pntlemf  26189  pntlemo  26191  ostth2lem3  26219  ostth3  26222  footeq  26518  hlperpnel  26519  perpdragALT  26521  perpdrag  26522  colperp  26523  mideulem2  26528  opphllem  26529  opphllem3  26543  lmieu  26578  trgcopy  26598  sacgr  26625  acopyeu  26628  usgredgleordALT  27024  eucrctshift  28028  nvabs  28455  smcnlem  28480  ubthlem2  28654  minvecolem4  28663  htthlem  28700  normpyc  28929  nmophmi  29814  hstle  30013  hstles  30014  stlei  30023  f1rnen  30388  fmptssfisupp  30445  nnmulge  30500  fsumiunle  30571  wrdt2ind  30653  xrge0npcan  30728  trsp2cyc  30815  archirngz  30868  archiabllem1a  30870  archiabllem2a  30873  archiabllem2c  30874  ornglmulle  30929  orngrmulle  30930  drngdimgt0  31104  lbsdiflsp0  31110  madjusmdetlem2  31181  esumpinfval  31442  esumpinfsum  31446  esumpcvgval  31447  esum2d  31462  esumiun  31463  dya2icoseg  31645  omssubadd  31668  carsgsigalem  31683  carsggect  31686  carsgclctunlem3  31688  omsmeas  31691  eulerpartlems  31728  sgnmulsgn  31917  signsplypnf  31930  signsply0  31931  reprlt  32000  reprinfz1  32003  hgt750lemc  32028  hgt750lemf  32034  pthhashvtx  32487  resconn  32606  sinccvglem  33028  circum  33030  btwnxfr  33630  nn0prpwlem  33783  dnibndlem2  33931  unblimceq0  33959  irrdiff  34740  poimirlem7  35064  mblfinlem3  35096  mblfinlem4  35097  itg2addnclem3  35110  ftc1anc  35138  isbnd3  35222  cntotbnd  35234  bfp  35262  rrndstprj2  35269  1cvrjat  36771  3atlem1  36779  3atlem6  36784  llnmlplnN  36835  2llnjaN  36862  2lplnja  36915  dalem57  37025  dalawlem11  37177  dalawlem12  37178  lhp2lt  37297  lhpj1  37318  lhpm0atN  37325  4atexlemex2  37367  lautm  37390  cdleme17b  37583  cdleme20j  37614  cdleme30a  37674  cdlemg4c  37908  cdlemg17a  37957  cdlemg31c  37995  trljco  38036  cdlemk46  38244  dia2dimlem2  38361  cdlemm10N  38414  cdlemn10  38502  dihmeetlem1N  38586  dihglblem5apreN  38587  dihmeetlem15N  38617  mapdat  38963  lcmineqlem19  39335  lcmineqlem20  39336  3lexlogpow5ineq2  39342  metakunt29  39378  2xp3dxp2ge1d  39387  factwoffsmonot  39388  rtprmirr  39502  fltnlta  39619  3cubeslem1  39625  irrapxlem1  39763  irrapxlem4  39766  pell1qrgaplem  39814  pellfundglb  39826  rmspecfund  39850  monotoddzzfi  39883  rmynn  39897  jm2.24nn  39900  jm2.17c  39903  jm2.24  39904  acongeq  39924  jm2.20nn  39938  jm2.26lem3  39942  jm2.27a  39946  jm2.27c  39948  rmydioph  39955  jm3.1lem2  39959  frlmpwfi  40042  areaquad  40166  rp-isfinite6  40226  frege129d  40464  leeq1d  40860  imo72b2  40878  cvgdvgrat  41017  radcnvrat  41018  hashnzfzclim  41026  isosctrlem1ALT  41640  cncmpmax  41661  iooabslt  42136  fmul01lt1lem2  42227  clim1fr1  42243  limcrecl  42271  climxrrelem  42391  liminflbuz2  42457  stoweidlem1  42643  stoweidlem11  42653  stoweidlem14  42656  stoweidlem24  42666  stoweidlem26  42668  wallispilem4  42710  wallispilem5  42711  stirlinglem1  42716  fourierdlem51  42799  fourierdlem65  42813  fouriersw  42873  2leaddle2  43855  sqrtpwpw2p  44055  lighneallem4a  44126  flnn0div2ge  44947  logbpw2m1  44981  amgmwlem  45330