Theorem eqbrtrrd 5122

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  dftpos4  8187  dif1en  9086  fodomfi  9212  fodomfiOLD  9230  fmptssfisupp  9297  resfifsupp  9300  cnfcom2lem  9610  dmttrcl  9630  ttrclselem2  9635  ficardadju  10110  enfin1ai  10294  pwcfsdom  10494  fpwwe2lem6  10547  fpwwe2  10554  canthp1lem1  10563  1nqenq  10873  prlem936  10958  lemulge11  12004  supaddc  12109  supmul1  12111  mul2lt0llt0  13011  mul2lt0lgt0  13012  xaddge0  13173  xadddi2  13212  ltexp2a  14089  leexp2a  14095  nnlesq  14128  digit1  14160  faclbnd4lem1  14216  faclbnd6  14222  facavg  14224  prsshashgt1  14333  nehash2  14397  abs3dif  15255  abs2dif  15256  limsupgre  15404  rlimclim1  15468  rlimuni  15473  rlimres2  15484  rlimcn1  15511  rlimcn1b  15512  recn2  15524  imcn2  15525  rlimo1  15540  o1rlimmul  15542  iserex  15580  isercoll  15591  caucvgrlem2  15598  caucvgr  15599  iseraltlem3  15607  summolem2a  15638  fsumge1  15720  o1fsum  15736  isumrpcl  15766  climcnds  15774  harmonic  15782  mertenslem1  15807  prodmolem2a  15857  ege2le3  16013  efgt1p2  16039  efgt1p  16040  eirrlem  16129  rpnnen2lem11  16149  fsumdvds  16235  bitsfzo  16362  bitsmod  16363  bitscmp  16365  mulgcd  16475  dvdssqlem  16493  nn0seqcvgd  16497  mulgcddvds  16582  rpdvds  16587  qden1elz  16684  phimullem  16706  hashgcdlem  16715  hashgcdeq  16717  pcdvdstr  16804  pockthg  16834  prmreclem1  16844  4sqlem11  16883  ramub1lem1  16954  ramub1lem2  16955  mreexexlem4d  17570  sscid  17748  latmlej21  18403  latmlej22  18404  lubel  18437  efginvrel1  19657  odadd2  19778  odadd  19779  gexexlem  19781  cyggex2  19826  ablfacrplem  19996  ablfac1c  20002  ablfac1eu  20004  pgpfac1lem3a  20007  isabvd  20745  ornglmulle  20800  orngrmulle  20801  mptscmfsuppd  20879  znrrg  21520  frlmphl  21736  frlmup1  21753  f1linds  21780  psdmplcl  22105  chcoeffeqlem  22829  lmcn2  23593  metrtri  24301  imasdsf1olem  24317  stdbdxmet  24459  nrmmetd  24518  nmmtri  24566  nlmvscnlem2  24629  blcvx  24742  recld2  24759  zdis  24761  opnreen  24776  cnheibor  24910  lebnumlem3  24918  nmoleub2lem3  25071  nmoleub2lem2  25072  nmoleub3  25075  ipcnlem2  25200  cmetcaulem  25244  nglmle  25258  cncmet  25278  csbren  25355  trirn  25356  minveclem4  25388  ovoliunlem1  25459  ovoliun2  25463  ovolscalem1  25470  ovolicopnf  25481  voliunlem2  25508  volsup  25513  ioorcl2  25529  uniiccvol  25537  uniioombllem4  25543  i1fd  25638  mbfi1fseqlem4  25675  itg2const2  25698  itg2eqa  25702  itg2split  25706  itg2i1fseqle  25711  itg2cnlem2  25719  dvcnv  25937  dveflem  25939  dvferm1lem  25944  dvlip2  25956  c1liplem1  25957  dvivthlem1  25969  lhop1lem  25974  dvcvx  25981  dvfsumle  25982  dvfsumleOLD  25983  dvfsumabs  25985  dvfsumlem4  25992  dvfsumrlim2  25995  ftc1a  26000  tdeglem4  26021  deg1pwle  26081  fta1blem  26132  aalioulem3  26298  aaliou2b  26305  ulmbdd  26363  ulmdvlem1  26365  itgulm  26373  pserdvlem2  26394  abelthlem3  26399  abelthlem5  26401  abelthlem6  26402  abelthlem7  26404  tanregt0  26504  argimlt0  26578  logdivlti  26585  logcnlem3  26609  logcnlem4  26610  logtayl  26625  logtayl2  26627  cxple2  26662  cxpcn3lem  26713  cxpaddle  26718  rtprmirr  26726  isosctrlem1  26784  atantayl  26903  efrlim  26935  efrlimOLD  26936  dfef2  26937  o1cxp  26941  cxp2lim  26943  divsqrtsumo1  26950  amgmlem  26956  logdifbnd  26960  emcllem7  26968  harmonicbnd4  26977  fsumharmonic  26978  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamucov  27004  lgamcvg2  27021  gamcvg2  27026  ftalem2  27040  basellem2  27048  basellem5  27051  basellem9  27055  vma1  27132  sqff1o  27148  fsumfldivdiaglem  27155  chtub  27179  fsumvma2  27181  chpchtsum  27186  chpub  27187  logfaclbnd  27189  logfacbnd3  27190  logfacrlim  27191  logexprlim  27192  bcmono  27244  bposlem2  27252  bposlem5  27255  bposlem6  27256  lgsne0  27302  lgsquadlem1  27347  lgsquadlem2  27348  2sqblem  27398  2sqmod  27403  chebbnd1lem1  27436  chtppilimlem1  27440  chtppilimlem2  27441  chpchtlim  27446  rplogsumlem1  27451  dchrvmasumiflem1  27468  dchrisum0flblem2  27476  dchrisum0fno1  27478  dchrisum0lem2a  27484  dchrisum0lem3  27486  dirith  27496  mulog2sumlem1  27501  mulog2sumlem2  27502  log2sumbnd  27511  selberglem2  27513  logdivbnd  27523  selberg3lem1  27524  selberg4lem1  27527  pntrsumbnd2  27534  pntrlog2bndlem1  27544  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntibndlem3  27559  pntlemb  27564  pntlemn  27567  pntlemr  27569  pntlemj  27570  pntlemf  27572  pntlemo  27574  ostth2lem3  27602  ostth3  27605  addsuniflem  27997  ltsp1d  28011  negsid  28037  negsunif  28051  negleft  28054  mulsuniflem  28145  precsexlem9  28211  n0sge0  28334  zcuts  28403  halfcut  28454  addhalfcut  28455  pw2cut2  28458  bdayfinbndlem1  28463  footeq  28796  hlperpnel  28797  perpdragALT  28799  perpdrag  28800  colperp  28801  mideulem2  28806  opphllem  28807  opphllem3  28821  lmieu  28856  trgcopy  28876  sacgr  28903  acopyeu  28906  usgredgleordALT  29307  eucrctshift  30318  nvabs  30747  smcnlem  30772  ubthlem2  30946  minvecolem4  30955  htthlem  30992  normpyc  31221  nmophmi  32106  hstle  32305  hstles  32306  stlei  32315  f1rnen  32706  nnmulge  32818  fsumiunle  32910  sgnmulsgn  32923  wrdt2ind  33035  xrge0npcan  33102  gsumwrd2dccat  33160  trsp2cyc  33205  archirngz  33271  archiabllem1a  33273  archiabllem2a  33276  archiabllem2c  33277  elrgspnlem1  33324  elrgspn  33328  elrgspnsubrunlem2  33330  rprmasso  33606  q1pdir  33684  r1pquslmic  33692  evlextv  33707  mplvrpmga  33710  mplvrpmrhm  33712  drngdimgt0  33775  lbsdiflsp0  33783  fldextrspundgle  33835  fldext2rspun  33839  minplyirredlem  33867  madjusmdetlem2  33985  esumpinfval  34230  esumpinfsum  34234  esumpcvgval  34235  esum2d  34250  esumiun  34251  dya2icoseg  34434  omssubadd  34457  carsgsigalem  34472  carsggect  34475  carsgclctunlem3  34477  omsmeas  34480  eulerpartlems  34517  signsplypnf  34707  signsply0  34708  reprlt  34776  reprinfz1  34779  hgt750lemc  34804  hgt750lemf  34810  pthhashvtx  35322  resconn  35440  sinccvglem  35866  circum  35868  btwnxfr  36250  nn0prpwlem  36516  dnibndlem2  36679  unblimceq0  36707  irrdiff  37531  poimirlem7  37828  mblfinlem3  37860  mblfinlem4  37861  itg2addnclem3  37874  ftc1anc  37902  isbnd3  37985  cntotbnd  37997  bfp  38025  rrndstprj2  38032  1cvrjat  39735  3atlem1  39743  3atlem6  39748  llnmlplnN  39799  2llnjaN  39826  2lplnja  39879  dalem57  39989  dalawlem11  40141  dalawlem12  40142  lhp2lt  40261  lhpj1  40282  lhpm0atN  40289  4atexlemex2  40331  lautm  40354  cdleme17b  40547  cdleme20j  40578  cdleme30a  40638  cdlemg4c  40872  cdlemg17a  40921  cdlemg31c  40959  trljco  41000  cdlemk46  41208  dia2dimlem2  41325  cdlemm10N  41378  cdlemn10  41466  dihmeetlem1N  41550  dihglblem5apreN  41551  dihmeetlem15N  41581  mapdat  41927  lcmineqlem19  42301  lcmineqlem20  42302  aks4d1p1p5  42329  aks4d1p8d2  42339  aks4d1p8  42341  aks4d1p9  42342  hashscontpow  42376  dvdsexpnn  42588  mullt0b1d  42738  selvvvval  42828  evlselv  42830  mhphflem  42839  fltnlta  42906  3cubeslem1  42926  irrapxlem1  43064  irrapxlem4  43067  pell1qrgaplem  43115  pellfundglb  43127  rmspecfund  43151  monotoddzzfi  43184  rmynn  43198  jm2.24nn  43201  jm2.17c  43204  jm2.24  43205  acongeq  43225  jm2.20nn  43239  jm2.26lem3  43243  jm2.27a  43247  jm2.27c  43249  rmydioph  43256  jm3.1lem2  43260  frlmpwfi  43340  areaquad  43458  cantnf2  43567  rp-isfinite6  43759  frege129d  44004  leeq1d  44398  imo72b2lem0  44406  imo72b2  44413  cvgdvgrat  44554  radcnvrat  44555  hashnzfzclim  44563  isosctrlem1ALT  45174  cncmpmax  45277  iooabslt  45745  fmul01lt1lem2  45831  clim1fr1  45847  limcrecl  45875  climxrrelem  45993  liminflbuz2  46059  dvnprodlem1  46190  stoweidlem1  46245  stoweidlem11  46255  stoweidlem14  46258  stoweidlem24  46268  stoweidlem26  46270  wallispilem4  46312  wallispilem5  46313  stirlinglem1  46318  fourierdlem51  46401  fourierdlem65  46415  fouriersw  46475  2leaddle2  47544  sqrtpwpw2p  47784  lighneallem4a  47854  flnn0div2ge  48779  logbpw2m1  48813  functermclem  49752  amgmwlem  50047