Theorem eqbrtrrd 5124

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

Syntax hints:   → wi 4   = wceq 1560   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  dftpos4  8225  dif1en  9130  fodomfi  9256  fmptssfisupp  9340  cnfcom2lem  9656  dmttrcl  9676  ttrclselem2  9681  ficardadju  10156  enfin1ai  10341  pwcfsdom  10541  fpwwe2lem6  10594  fpwwe2  10601  canthp1lem1  10610  1nqenq  10920  prlem936  11005  lemulge11  12054  supaddc  12159  supmul1  12161  mul2lt0llt0  13099  mul2lt0lgt0  13100  xaddge0  13261  xadddi2  13300  ltexp2a  14179  leexp2a  14185  nnlesq  14218  digit1  14250  faclbnd4lem1  14306  faclbnd6  14312  facavg  14314  prsshashgt1  14423  nehash2  14487  sgnmulsgn  15122  abs3dif  15359  abs2dif  15360  limsupgre  15508  rlimclim1  15572  rlimuni  15577  rlimres2  15588  rlimcn1  15615  rlimcn1b  15616  recn2  15628  imcn2  15629  rlimo1  15644  o1rlimmul  15646  iserex  15684  isercoll  15695  caucvgrlem2  15702  caucvgr  15703  iseraltlem3  15711  summolem2a  15742  fsumge1  15825  o1fsum  15841  isumrpcl  15873  climcnds  15881  harmonic  15889  mertenslem1  15914  prodmolem2a  15964  ege2le3  16120  efgt1p2  16146  efgt1p  16147  eirrlem  16236  rpnnen2lem11  16256  fsumdvds  16342  bitsfzo  16469  bitsmod  16470  bitscmp  16472  mulgcd  16582  dvdssqlem  16600  nn0seqcvgd  16604  mulgcddvds  16689  rpdvds  16694  qden1elz  16792  phimullem  16814  hashgcdlem  16823  hashgcdeq  16825  pcdvdstr  16912  pockthg  16942  prmreclem1  16952  4sqlem11  16991  ramub1lem1  17062  ramub1lem2  17063  mreexexlem4d  17679  sscid  17857  latmlej21  18512  latmlej22  18513  lubel  18546  efginvrel1  19768  odadd2  19889  odadd  19890  gexexlem  19892  cyggex2  19937  ablfacrplem  20107  ablfac1c  20113  ablfac1eu  20115  pgpfac1lem3a  20118  isabvd  20861  ornglmulle  20916  orngrmulle  20917  mptscmfsuppd  20995  znrrg  21617  frlmphl  21833  frlmup1  21850  f1linds  21877  selvvvval  22195  psdmplcl  22227  chcoeffeqlem  22945  lmcn2  23709  metrtri  24417  imasdsf1olem  24433  stdbdxmet  24575  nrmmetd  24634  nmmtri  24682  nlmvscnlem2  24745  blcvx  24858  recld2  24875  zdis  24877  opnreen  24892  cnheibor  25017  lebnumlem3  25025  nmoleub2lem3  25177  nmoleub2lem2  25178  nmoleub3  25181  ipcnlem2  25306  cmetcaulem  25350  nglmle  25364  cncmet  25384  csbren  25461  trirn  25462  minveclem4  25494  ovoliunlem1  25564  ovoliun2  25568  ovolscalem1  25575  ovolicopnf  25586  voliunlem2  25613  volsup  25618  ioorcl2  25634  uniiccvol  25642  uniioombllem4  25648  i1fd  25743  mbfi1fseqlem4  25780  itg2const2  25803  itg2eqa  25807  itg2split  25811  itg2i1fseqle  25816  itg2cnlem2  25824  dvcnv  26039  dveflem  26041  dvferm1lem  26046  dvlip2  26057  c1liplem1  26058  dvivthlem1  26070  lhop1lem  26075  dvcvx  26082  dvfsumle  26083  dvfsumabs  26085  dvfsumlem4  26091  dvfsumrlim2  26094  ftc1a  26099  tdeglem4  26120  deg1pwle  26180  fta1blem  26231  aalioulem3  26398  aaliou2b  26405  ulmbdd  26461  ulmdvlem1  26463  itgulm  26471  pserdvlem2  26491  abelthlem3  26496  abelthlem5  26498  abelthlem6  26499  abelthlem7  26501  tanregt0  26604  argimlt0  26678  logdivlti  26685  logcnlem3  26709  logcnlem4  26710  logtayl  26725  logtayl2  26727  cxple2  26762  cxpcn3lem  26812  cxpaddle  26817  rtprmirr  26825  isosctrlem1  26883  atantayl  27002  efrlim  27034  dfef2  27035  o1cxp  27039  cxp2lim  27041  divsqrtsumo1  27048  amgmlem  27054  logdifbnd  27058  emcllem7  27066  harmonicbnd4  27075  fsumharmonic  27076  lgamgulmlem2  27094  lgamgulmlem3  27095  lgamucov  27102  lgamcvg2  27119  gamcvg2  27124  ftalem2  27138  basellem2  27146  basellem5  27149  basellem9  27153  vma1  27230  sqff1o  27246  fsumfldivdiaglem  27253  chtub  27276  fsumvma2  27278  chpchtsum  27283  chpub  27284  logfaclbnd  27286  logfacbnd3  27287  logfacrlim  27288  logexprlim  27289  bcmono  27341  bposlem2  27349  bposlem5  27352  bposlem6  27353  lgsne0  27399  lgsquadlem1  27444  lgsquadlem2  27445  2sqblem  27495  2sqmod  27500  chebbnd1lem1  27533  chtppilimlem1  27537  chtppilimlem2  27538  chpchtlim  27543  rplogsumlem1  27548  dchrvmasumiflem1  27565  dchrisum0flblem2  27573  dchrisum0fno1  27575  dchrisum0lem2a  27581  dchrisum0lem3  27583  dirith  27593  mulog2sumlem1  27598  mulog2sumlem2  27599  log2sumbnd  27608  selberglem2  27610  logdivbnd  27620  selberg3lem1  27621  selberg4lem1  27624  pntrsumbnd2  27631  pntrlog2bndlem1  27641  pntrlog2bndlem5  27645  pntrlog2bndlem6  27647  pntpbnd1a  27649  pntpbnd1  27650  pntpbnd2  27651  pntibndlem3  27656  pntlemb  27661  pntlemn  27664  pntlemr  27666  pntlemj  27667  pntlemf  27669  pntlemo  27671  ostth2lem3  27699  ostth3  27702  addsuniflem  28094  ltsp1d  28108  negsid  28134  negsunif  28148  negleft  28151  mulsuniflem  28242  precsexlem9  28308  n0sge0  28431  zcuts  28500  halfcut  28551  addhalfcut  28552  pw2cut2  28555  bdayfinbndlem1  28560  footeq  28897  hlperpnel  28898  perpdragALT  28900  perpdrag  28901  colperp  28902  mideulem2  28907  opphllem  28908  opphllem3  28922  lmieu  28957  trgcopy  28977  sacgr  29025  acopyeu  29028  usgredgleordALT  29435  eucrctshift  30445  nvabs  30875  smcnlem  30900  ubthlem2  31074  minvecolem4  31083  htthlem  31120  normpyc  31349  nmophmi  32234  hstle  32433  hstles  32434  stlei  32443  f1rnen  32830  nnmulge  32941  fsumiunle  33031  wrdt2ind  33131  xrge0npcan  33198  gsumwrd2dccat  33258  trsp2cyc  33303  archirngz  33369  archiabllem1a  33371  archiabllem2a  33374  archiabllem2c  33375  elrgspnlem1  33423  elrgspn  33427  elrgspnsubrunlem2  33429  rprmasso  33721  q1pdir  33799  r1pquslmic  33807  selvply1rhmlema  33815  selvply1rhmlem1  33817  evlextv  33839  mplvrpmga  33842  mplvrpmrhm  33844  drngdimgt0  33915  lbsdiflsp0  33923  fldextrspundgle  33975  fldext2rspun  33979  minplyirredlem  34007  madjusmdetlem2  34125  esumpinfval  34370  esumpinfsum  34374  esumpcvgval  34375  esum2d  34390  esumiun  34391  dya2icoseg  34574  omssubadd  34597  carsgsigalem  34612  carsggect  34615  carsgclctunlem3  34617  omsmeas  34620  eulerpartlems  34657  signsplypnf  34844  signsply0  34845  reprlt  34913  reprinfz1  34916  hgt750lemc  34941  hgt750lemf  34947  pthhashvtx  35478  resconn  35596  sinccvglem  36022  circum  36024  btwnxfr  36406  nn0prpwlem  36682  dnibndlem2  36917  unblimceq0  36945  irrdiff  37818  poimirlem7  38126  mblfinlem3  38158  mblfinlem4  38159  itg2addnclem3  38172  ftc1anc  38200  isbnd3  38283  cntotbnd  38295  bfp  38323  rrndstprj2  38330  1cvrjat  40099  3atlem1  40107  3atlem6  40112  llnmlplnN  40163  2llnjaN  40190  2lplnja  40243  dalem57  40353  dalawlem11  40505  dalawlem12  40506  lhp2lt  40625  lhpj1  40646  lhpm0atN  40653  4atexlemex2  40695  lautm  40718  cdleme17b  40911  cdleme20j  40942  cdleme30a  41002  cdlemg4c  41236  cdlemg17a  41285  cdlemg31c  41323  trljco  41364  cdlemk46  41572  dia2dimlem2  41689  cdlemm10N  41742  cdlemn10  41830  dihmeetlem1N  41914  dihglblem5apreN  41915  dihmeetlem15N  41945  mapdat  42291  lcmineqlem19  42664  lcmineqlem20  42665  aks4d1p1p5  42692  aks4d1p8d2  42702  aks4d1p8  42704  aks4d1p9  42705  hashscontpow  42739  dvdsexpnn  42942  mullt0b1d  43105  evlselv  43171  mhphflem  43178  fltnlta  43245  3cubeslem1  43265  irrapxlem1  43399  irrapxlem4  43402  pell1qrgaplem  43450  pellfundglb  43462  rmspecfund  43486  monotoddzzfi  43519  rmynn  43533  jm2.24nn  43536  jm2.17c  43539  jm2.24  43540  acongeq  43560  jm2.20nn  43574  jm2.26lem3  43578  jm2.27a  43582  jm2.27c  43584  rmydioph  43591  jm3.1lem2  43595  frlmpwfi  43675  areaquad  43793  cantnf2  43902  rp-isfinite6  44094  frege129d  44339  leeq1d  44733  imo72b2lem0  44741  imo72b2  44748  cvgdvgrat  44889  radcnvrat  44890  hashnzfzclim  44898  isosctrlem1ALT  45509  cncmpmax  45612  iooabslt  46075  fmul01lt1lem2  46161  clim1fr1  46177  limcrecl  46205  climxrrelem  46323  liminflbuz2  46389  dvnprodlem1  46520  stoweidlem1  46575  stoweidlem11  46585  stoweidlem14  46588  stoweidlem24  46598  stoweidlem26  46600  wallispilem4  46642  wallispilem5  46643  stirlinglem1  46648  fourierdlem51  46731  fourierdlem65  46745  fouriersw  46805  2leaddle2  47892  2timesltsqm1  47973  sqrtpwpw2p  48147  lighneallem4a  48217  flnn0div2ge  49155  logbpw2m1  49189  functermclem  50128  amgmwlem  50423