Theorem eqbrtrrd 5096

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  dftpos4  8185  dif1en  9086  fodomfi  9212  fodomfiOLD  9230  fmptssfisupp  9297  resfifsupp  9300  cnfcom2lem  9613  dmttrcl  9633  ttrclselem2  9638  ficardadju  10113  enfin1ai  10297  pwcfsdom  10497  fpwwe2lem6  10550  fpwwe2  10557  canthp1lem1  10566  1nqenq  10876  prlem936  10961  lemulge11  12009  supaddc  12114  supmul1  12116  mul2lt0llt0  13039  mul2lt0lgt0  13040  xaddge0  13201  xadddi2  13240  ltexp2a  14119  leexp2a  14125  nnlesq  14158  digit1  14190  faclbnd4lem1  14246  faclbnd6  14252  facavg  14254  prsshashgt1  14363  nehash2  14427  abs3dif  15285  abs2dif  15286  limsupgre  15434  rlimclim1  15498  rlimuni  15503  rlimres2  15514  rlimcn1  15541  rlimcn1b  15542  recn2  15554  imcn2  15555  rlimo1  15570  o1rlimmul  15572  iserex  15610  isercoll  15621  caucvgrlem2  15628  caucvgr  15629  iseraltlem3  15637  summolem2a  15668  fsumge1  15751  o1fsum  15767  isumrpcl  15799  climcnds  15807  harmonic  15815  mertenslem1  15840  prodmolem2a  15890  ege2le3  16046  efgt1p2  16072  efgt1p  16073  eirrlem  16162  rpnnen2lem11  16182  fsumdvds  16268  bitsfzo  16395  bitsmod  16396  bitscmp  16398  mulgcd  16508  dvdssqlem  16526  nn0seqcvgd  16530  mulgcddvds  16615  rpdvds  16620  qden1elz  16718  phimullem  16740  hashgcdlem  16749  hashgcdeq  16751  pcdvdstr  16838  pockthg  16868  prmreclem1  16878  4sqlem11  16917  ramub1lem1  16988  ramub1lem2  16989  mreexexlem4d  17604  sscid  17782  latmlej21  18437  latmlej22  18438  lubel  18471  efginvrel1  19694  odadd2  19815  odadd  19816  gexexlem  19818  cyggex2  19863  ablfacrplem  20033  ablfac1c  20039  ablfac1eu  20041  pgpfac1lem3a  20044  isabvd  20784  ornglmulle  20839  orngrmulle  20840  mptscmfsuppd  20918  znrrg  21540  frlmphl  21756  frlmup1  21773  f1linds  21800  selvvvval  22118  psdmplcl  22150  chcoeffeqlem  22868  lmcn2  23632  metrtri  24340  imasdsf1olem  24356  stdbdxmet  24498  nrmmetd  24557  nmmtri  24605  nlmvscnlem2  24668  blcvx  24781  recld2  24798  zdis  24800  opnreen  24815  cnheibor  24940  lebnumlem3  24948  nmoleub2lem3  25100  nmoleub2lem2  25101  nmoleub3  25104  ipcnlem2  25229  cmetcaulem  25273  nglmle  25287  cncmet  25307  csbren  25384  trirn  25385  minveclem4  25417  ovoliunlem1  25487  ovoliun2  25491  ovolscalem1  25498  ovolicopnf  25509  voliunlem2  25536  volsup  25541  ioorcl2  25557  uniiccvol  25565  uniioombllem4  25571  i1fd  25666  mbfi1fseqlem4  25703  itg2const2  25726  itg2eqa  25730  itg2split  25734  itg2i1fseqle  25739  itg2cnlem2  25747  dvcnv  25962  dveflem  25964  dvferm1lem  25969  dvlip2  25980  c1liplem1  25981  dvivthlem1  25993  lhop1lem  25998  dvcvx  26005  dvfsumle  26006  dvfsumabs  26008  dvfsumlem4  26014  dvfsumrlim2  26017  ftc1a  26022  tdeglem4  26043  deg1pwle  26103  fta1blem  26154  aalioulem3  26318  aaliou2b  26325  ulmbdd  26381  ulmdvlem1  26383  itgulm  26391  pserdvlem2  26411  abelthlem3  26416  abelthlem5  26418  abelthlem6  26419  abelthlem7  26421  tanregt0  26521  argimlt0  26595  logdivlti  26602  logcnlem3  26626  logcnlem4  26627  logtayl  26642  logtayl2  26644  cxple2  26679  cxpcn3lem  26729  cxpaddle  26734  rtprmirr  26742  isosctrlem1  26800  atantayl  26919  efrlim  26951  dfef2  26952  o1cxp  26956  cxp2lim  26958  divsqrtsumo1  26965  amgmlem  26971  logdifbnd  26975  emcllem7  26983  harmonicbnd4  26992  fsumharmonic  26993  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamucov  27019  lgamcvg2  27036  gamcvg2  27041  ftalem2  27055  basellem2  27063  basellem5  27066  basellem9  27070  vma1  27147  sqff1o  27163  fsumfldivdiaglem  27170  chtub  27193  fsumvma2  27195  chpchtsum  27200  chpub  27201  logfaclbnd  27203  logfacbnd3  27204  logfacrlim  27205  logexprlim  27206  bcmono  27258  bposlem2  27266  bposlem5  27269  bposlem6  27270  lgsne0  27316  lgsquadlem1  27361  lgsquadlem2  27362  2sqblem  27412  2sqmod  27417  chebbnd1lem1  27450  chtppilimlem1  27454  chtppilimlem2  27455  chpchtlim  27460  rplogsumlem1  27465  dchrvmasumiflem1  27482  dchrisum0flblem2  27490  dchrisum0fno1  27492  dchrisum0lem2a  27498  dchrisum0lem3  27500  dirith  27510  mulog2sumlem1  27515  mulog2sumlem2  27516  log2sumbnd  27525  selberglem2  27527  logdivbnd  27537  selberg3lem1  27538  selberg4lem1  27541  pntrsumbnd2  27548  pntrlog2bndlem1  27558  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntibndlem3  27573  pntlemb  27578  pntlemn  27581  pntlemr  27583  pntlemj  27584  pntlemf  27586  pntlemo  27588  ostth2lem3  27616  ostth3  27619  addsuniflem  28011  ltsp1d  28025  negsid  28051  negsunif  28065  negleft  28068  mulsuniflem  28159  precsexlem9  28225  n0sge0  28348  zcuts  28417  halfcut  28468  addhalfcut  28469  pw2cut2  28472  bdayfinbndlem1  28477  footeq  28810  hlperpnel  28811  perpdragALT  28813  perpdrag  28814  colperp  28815  mideulem2  28820  opphllem  28821  opphllem3  28835  lmieu  28870  trgcopy  28890  sacgr  28917  acopyeu  28920  usgredgleordALT  29321  eucrctshift  30331  nvabs  30761  smcnlem  30786  ubthlem2  30960  minvecolem4  30969  htthlem  31006  normpyc  31235  nmophmi  32120  hstle  32319  hstles  32320  stlei  32329  f1rnen  32720  nnmulge  32831  fsumiunle  32921  sgnmulsgn  32934  wrdt2ind  33032  xrge0npcan  33099  gsumwrd2dccat  33159  trsp2cyc  33204  archirngz  33270  archiabllem1a  33272  archiabllem2a  33275  archiabllem2c  33276  elrgspnlem1  33323  elrgspn  33327  elrgspnsubrunlem2  33329  rprmasso  33608  q1pdir  33686  r1pquslmic  33694  selvply1rhmlema  33702  selvply1rhmlem1  33704  evlextv  33726  mplvrpmga  33729  mplvrpmrhm  33731  drngdimgt0  33802  lbsdiflsp0  33810  fldextrspundgle  33862  fldext2rspun  33866  minplyirredlem  33894  madjusmdetlem2  34012  esumpinfval  34257  esumpinfsum  34261  esumpcvgval  34262  esum2d  34277  esumiun  34278  dya2icoseg  34461  omssubadd  34484  carsgsigalem  34499  carsggect  34502  carsgclctunlem3  34504  omsmeas  34507  eulerpartlems  34544  signsplypnf  34734  signsply0  34735  reprlt  34803  reprinfz1  34806  hgt750lemc  34831  hgt750lemf  34837  pthhashvtx  35356  resconn  35474  sinccvglem  35900  circum  35902  btwnxfr  36284  nn0prpwlem  36550  dnibndlem2  36785  unblimceq0  36813  irrdiff  37686  poimirlem7  37994  mblfinlem3  38026  mblfinlem4  38027  itg2addnclem3  38040  ftc1anc  38068  isbnd3  38151  cntotbnd  38163  bfp  38191  rrndstprj2  38198  1cvrjat  39967  3atlem1  39975  3atlem6  39980  llnmlplnN  40031  2llnjaN  40058  2lplnja  40111  dalem57  40221  dalawlem11  40373  dalawlem12  40374  lhp2lt  40493  lhpj1  40514  lhpm0atN  40521  4atexlemex2  40563  lautm  40586  cdleme17b  40779  cdleme20j  40810  cdleme30a  40870  cdlemg4c  41104  cdlemg17a  41153  cdlemg31c  41191  trljco  41232  cdlemk46  41440  dia2dimlem2  41557  cdlemm10N  41610  cdlemn10  41698  dihmeetlem1N  41782  dihglblem5apreN  41783  dihmeetlem15N  41813  mapdat  42159  lcmineqlem19  42532  lcmineqlem20  42533  aks4d1p1p5  42560  aks4d1p8d2  42570  aks4d1p8  42572  aks4d1p9  42573  hashscontpow  42607  dvdsexpnn  42810  mullt0b1d  42973  evlselv  43039  mhphflem  43046  fltnlta  43113  3cubeslem1  43133  irrapxlem1  43267  irrapxlem4  43270  pell1qrgaplem  43318  pellfundglb  43330  rmspecfund  43354  monotoddzzfi  43387  rmynn  43401  jm2.24nn  43404  jm2.17c  43407  jm2.24  43408  acongeq  43428  jm2.20nn  43442  jm2.26lem3  43446  jm2.27a  43450  jm2.27c  43452  rmydioph  43459  jm3.1lem2  43463  frlmpwfi  43543  areaquad  43661  cantnf2  43770  rp-isfinite6  43962  frege129d  44207  leeq1d  44601  imo72b2lem0  44609  imo72b2  44616  cvgdvgrat  44757  radcnvrat  44758  hashnzfzclim  44766  isosctrlem1ALT  45377  cncmpmax  45480  iooabslt  45944  fmul01lt1lem2  46030  clim1fr1  46046  limcrecl  46074  climxrrelem  46192  liminflbuz2  46258  dvnprodlem1  46389  stoweidlem1  46444  stoweidlem11  46454  stoweidlem14  46457  stoweidlem24  46467  stoweidlem26  46469  wallispilem4  46511  wallispilem5  46512  stirlinglem1  46517  fourierdlem51  46600  fourierdlem65  46614  fouriersw  46674  2leaddle2  47761  2timesltsqm1  47842  sqrtpwpw2p  48016  lighneallem4a  48086  flnn0div2ge  49024  logbpw2m1  49058  functermclem  49997  amgmwlem  50292