Theorem eqbrtrrd 5178

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

Syntax hints:   → wi 4   = wceq 1534   class class class wbr 5154

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-ext 2700

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2062  df-clab 2707  df-cleq 2721  df-clel 2806  df-rab 3429  df-v 3474  df-dif 3961  df-un 3963  df-ss 3975  df-nul 4334  df-if 4535  df-sn 4635  df-pr 4637  df-op 4641  df-br 5155

This theorem is referenced by:  dftpos4  8264  dif1en  9201  dif1enOLD  9203  fodomfi  9353  fodomfiOLD  9373  fmptssfisupp  9438  resfifsupp  9441  cnfcom2lem  9745  dmttrcl  9765  ttrclselem2  9770  ficardadju  10244  enfin1ai  10428  pwcfsdom  10627  fpwwe2lem6  10680  fpwwe2  10687  canthp1lem1  10696  1nqenq  11006  prlem936  11091  lemulge11  12132  supaddc  12237  supmul1  12239  mul2lt0llt0  13136  mul2lt0lgt0  13137  xaddge0  13295  xadddi2  13334  ltexp2a  14190  leexp2a  14196  nnlesq  14228  digit1  14260  faclbnd4lem1  14316  faclbnd6  14322  facavg  14324  prsshashgt1  14433  nehash2  14497  abs3dif  15349  abs2dif  15350  limsupgre  15496  rlimclim1  15560  rlimuni  15565  rlimres2  15576  rlimcn1  15603  rlimcn1b  15604  recn2  15616  imcn2  15617  rlimo1  15632  o1rlimmul  15634  iserex  15674  isercoll  15685  caucvgrlem2  15692  caucvgr  15693  iseraltlem3  15701  summolem2a  15732  fsumge1  15814  o1fsum  15830  isumrpcl  15860  climcnds  15868  harmonic  15876  mertenslem1  15901  prodmolem2a  15949  ege2le3  16105  efgt1p2  16129  efgt1p  16130  eirrlem  16219  rpnnen2lem11  16239  fsumdvds  16323  bitsfzo  16448  bitsmod  16449  bitscmp  16451  mulgcd  16562  dvdssqlem  16580  nn0seqcvgd  16584  mulgcddvds  16669  rpdvds  16674  qden1elz  16772  phimullem  16794  hashgcdlem  16803  hashgcdeq  16804  pcdvdstr  16891  pockthg  16921  prmreclem1  16931  4sqlem11  16970  ramub1lem1  17041  ramub1lem2  17042  mreexexlem4d  17673  sscid  17853  latmlej21  18518  latmlej22  18519  lubel  18552  efginvrel1  19738  odadd2  19859  odadd  19860  gexexlem  19862  cyggex2  19907  ablfacrplem  20077  ablfac1c  20083  ablfac1eu  20085  pgpfac1lem3a  20088  isabvd  20803  mptscmfsuppd  20916  znrrg  21575  frlmphl  21792  frlmup1  21809  f1linds  21836  psdmplcl  22155  chcoeffeqlem  22878  lmcn2  23644  metrtri  24354  imasdsf1olem  24370  stdbdxmet  24515  nrmmetd  24574  nmmtri  24622  nlmvscnlem2  24693  blcvx  24805  recld2  24821  zdis  24823  opnreen  24838  cnheibor  24972  lebnumlem3  24980  nmoleub2lem3  25133  nmoleub2lem2  25134  nmoleub3  25137  ipcnlem2  25263  cmetcaulem  25307  nglmle  25321  cncmet  25341  csbren  25418  trirn  25419  minveclem4  25451  ovoliunlem1  25522  ovoliun2  25526  ovolscalem1  25533  ovolicopnf  25544  voliunlem2  25571  volsup  25576  ioorcl2  25592  uniiccvol  25600  uniioombllem4  25606  i1fd  25701  mbfi1fseqlem4  25739  itg2const2  25762  itg2eqa  25766  itg2split  25770  itg2i1fseqle  25775  itg2cnlem2  25783  dvcnv  26000  dveflem  26002  dvferm1lem  26007  dvlip2  26019  c1liplem1  26020  dvivthlem1  26032  lhop1lem  26037  dvcvx  26044  dvfsumle  26045  dvfsumleOLD  26046  dvfsumabs  26048  dvfsumlem4  26055  dvfsumrlim2  26058  ftc1a  26063  tdeglem4  26084  deg1pwle  26144  fta1blem  26195  aalioulem3  26359  aaliou2b  26366  ulmbdd  26424  ulmdvlem1  26426  itgulm  26434  pserdvlem2  26455  abelthlem3  26460  abelthlem5  26462  abelthlem6  26463  abelthlem7  26465  tanregt0  26563  argimlt0  26637  logdivlti  26644  logcnlem3  26668  logcnlem4  26669  logtayl  26684  logtayl2  26686  cxple2  26721  cxpcn3lem  26772  cxpaddle  26777  rtprmirr  26785  isosctrlem1  26843  atantayl  26962  efrlim  26994  efrlimOLD  26995  dfef2  26996  o1cxp  27000  cxp2lim  27002  divsqrtsumo1  27009  amgmlem  27015  logdifbnd  27019  emcllem7  27027  harmonicbnd4  27036  fsumharmonic  27037  lgamgulmlem2  27055  lgamgulmlem3  27056  lgamucov  27063  lgamcvg2  27080  gamcvg2  27085  ftalem2  27099  basellem2  27107  basellem5  27110  basellem9  27114  vma1  27191  sqff1o  27207  fsumfldivdiaglem  27214  chtub  27238  fsumvma2  27240  chpchtsum  27245  chpub  27246  logfaclbnd  27248  logfacbnd3  27249  logfacrlim  27250  logexprlim  27251  bcmono  27303  bposlem2  27311  bposlem5  27314  bposlem6  27315  lgsne0  27361  lgsquadlem1  27406  lgsquadlem2  27407  2sqblem  27457  2sqmod  27462  chebbnd1lem1  27495  chtppilimlem1  27499  chtppilimlem2  27500  chpchtlim  27505  rplogsumlem1  27510  dchrvmasumiflem1  27527  dchrisum0flblem2  27535  dchrisum0fno1  27537  dchrisum0lem2a  27543  dchrisum0lem3  27545  dirith  27555  mulog2sumlem1  27560  mulog2sumlem2  27561  log2sumbnd  27570  selberglem2  27572  logdivbnd  27582  selberg3lem1  27583  selberg4lem1  27586  pntrsumbnd2  27593  pntrlog2bndlem1  27603  pntrlog2bndlem5  27607  pntrlog2bndlem6  27609  pntpbnd1a  27611  pntpbnd1  27612  pntpbnd2  27613  pntibndlem3  27618  pntlemb  27623  pntlemn  27626  pntlemr  27628  pntlemj  27629  pntlemf  27631  pntlemo  27633  ostth2lem3  27661  ostth3  27664  addsuniflem  28012  negsid  28048  negsunif  28062  mulsuniflem  28149  precsexlem9  28213  om2noseqlt  28273  n0sge0  28309  uzsind  28358  footeq  28693  hlperpnel  28694  perpdragALT  28696  perpdrag  28697  colperp  28698  mideulem2  28703  opphllem  28704  opphllem3  28718  lmieu  28753  trgcopy  28773  sacgr  28800  acopyeu  28803  usgredgleordALT  29212  eucrctshift  30218  nvabs  30647  smcnlem  30672  ubthlem2  30846  minvecolem4  30855  htthlem  30892  normpyc  31121  nmophmi  32006  hstle  32205  hstles  32206  stlei  32215  f1rnen  32592  nnmulge  32697  fsumiunle  32778  wrdt2ind  32865  xrge0npcan  32951  trsp2cyc  33061  archirngz  33114  archiabllem1a  33116  archiabllem2a  33119  archiabllem2c  33120  ornglmulle  33245  orngrmulle  33246  rprmasso  33463  q1pdir  33533  r1pquslmic  33541  drngdimgt0  33576  lbsdiflsp0  33584  minplyirredlem  33648  madjusmdetlem2  33719  esumpinfval  33982  esumpinfsum  33986  esumpcvgval  33987  esum2d  34002  esumiun  34003  dya2icoseg  34187  omssubadd  34210  carsgsigalem  34225  carsggect  34228  carsgclctunlem3  34230  omsmeas  34233  eulerpartlems  34270  sgnmulsgn  34459  signsplypnf  34472  signsply0  34473  reprlt  34541  reprinfz1  34544  hgt750lemc  34569  hgt750lemf  34575  pthhashvtx  35040  resconn  35159  sinccvglem  35585  circum  35587  btwnxfr  35965  nn0prpwlem  36120  dnibndlem2  36268  unblimceq0  36296  irrdiff  37118  poimirlem7  37413  mblfinlem3  37445  mblfinlem4  37446  itg2addnclem3  37459  ftc1anc  37487  isbnd3  37570  cntotbnd  37582  bfp  37610  rrndstprj2  37617  1cvrjat  39259  3atlem1  39267  3atlem6  39272  llnmlplnN  39323  2llnjaN  39350  2lplnja  39403  dalem57  39513  dalawlem11  39665  dalawlem12  39666  lhp2lt  39785  lhpj1  39806  lhpm0atN  39813  4atexlemex2  39855  lautm  39878  cdleme17b  40071  cdleme20j  40102  cdleme30a  40162  cdlemg4c  40396  cdlemg17a  40445  cdlemg31c  40483  trljco  40524  cdlemk46  40732  dia2dimlem2  40849  cdlemm10N  40902  cdlemn10  40990  dihmeetlem1N  41074  dihglblem5apreN  41075  dihmeetlem15N  41105  mapdat  41451  lcmineqlem19  41831  lcmineqlem20  41832  aks4d1p1p5  41859  aks4d1p8d2  41869  aks4d1p8  41871  aks4d1p9  41872  hashscontpow  41906  metakunt29  42016  2xp3dxp2ge1d  42024  factwoffsmonot  42025  dvdsexpnn  42134  selvvvval  42350  evlselv  42352  mhphflem  42361  fltnlta  42428  3cubeslem1  42453  irrapxlem1  42591  irrapxlem4  42594  pell1qrgaplem  42642  pellfundglb  42654  rmspecfund  42678  monotoddzzfi  42712  rmynn  42726  jm2.24nn  42729  jm2.17c  42732  jm2.24  42733  acongeq  42753  jm2.20nn  42767  jm2.26lem3  42771  jm2.27a  42775  jm2.27c  42777  rmydioph  42784  jm3.1lem2  42788  frlmpwfi  42871  areaquad  42993  cantnf2  43103  rp-isfinite6  43297  frege129d  43542  leeq1d  43936  imo72b2  43951  cvgdvgrat  44099  radcnvrat  44100  hashnzfzclim  44108  isosctrlem1ALT  44722  cncmpmax  44743  iooabslt  45228  fmul01lt1lem2  45317  clim1fr1  45333  limcrecl  45361  climxrrelem  45481  liminflbuz2  45547  stoweidlem1  45733  stoweidlem11  45743  stoweidlem14  45746  stoweidlem24  45756  stoweidlem26  45758  wallispilem4  45800  wallispilem5  45801  stirlinglem1  45806  fourierdlem51  45889  fourierdlem65  45903  fouriersw  45963  2leaddle2  47022  sqrtpwpw2p  47221  lighneallem4a  47291  flnn0div2ge  48043  logbpw2m1  48077  amgmwlem  48672