Theorem eqbrtrrd 5131

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  dftpos4  8224  dif1en  9124  dif1enOLD  9126  fodomfi  9261  fodomfiOLD  9281  fmptssfisupp  9345  resfifsupp  9348  cnfcom2lem  9654  dmttrcl  9674  ttrclselem2  9679  ficardadju  10153  enfin1ai  10337  pwcfsdom  10536  fpwwe2lem6  10589  fpwwe2  10596  canthp1lem1  10605  1nqenq  10915  prlem936  11000  lemulge11  12045  supaddc  12150  supmul1  12152  mul2lt0llt0  13057  mul2lt0lgt0  13058  xaddge0  13218  xadddi2  13257  ltexp2a  14131  leexp2a  14137  nnlesq  14170  digit1  14202  faclbnd4lem1  14258  faclbnd6  14264  facavg  14266  prsshashgt1  14375  nehash2  14439  abs3dif  15298  abs2dif  15299  limsupgre  15447  rlimclim1  15511  rlimuni  15516  rlimres2  15527  rlimcn1  15554  rlimcn1b  15555  recn2  15567  imcn2  15568  rlimo1  15583  o1rlimmul  15585  iserex  15623  isercoll  15634  caucvgrlem2  15641  caucvgr  15642  iseraltlem3  15650  summolem2a  15681  fsumge1  15763  o1fsum  15779  isumrpcl  15809  climcnds  15817  harmonic  15825  mertenslem1  15850  prodmolem2a  15900  ege2le3  16056  efgt1p2  16082  efgt1p  16083  eirrlem  16172  rpnnen2lem11  16192  fsumdvds  16278  bitsfzo  16405  bitsmod  16406  bitscmp  16408  mulgcd  16518  dvdssqlem  16536  nn0seqcvgd  16540  mulgcddvds  16625  rpdvds  16630  qden1elz  16727  phimullem  16749  hashgcdlem  16758  hashgcdeq  16760  pcdvdstr  16847  pockthg  16877  prmreclem1  16887  4sqlem11  16926  ramub1lem1  16997  ramub1lem2  16998  mreexexlem4d  17608  sscid  17786  latmlej21  18439  latmlej22  18440  lubel  18473  efginvrel1  19658  odadd2  19779  odadd  19780  gexexlem  19782  cyggex2  19827  ablfacrplem  19997  ablfac1c  20003  ablfac1eu  20005  pgpfac1lem3a  20008  isabvd  20721  mptscmfsuppd  20834  znrrg  21475  frlmphl  21690  frlmup1  21707  f1linds  21734  psdmplcl  22049  chcoeffeqlem  22772  lmcn2  23536  metrtri  24245  imasdsf1olem  24261  stdbdxmet  24403  nrmmetd  24462  nmmtri  24510  nlmvscnlem2  24573  blcvx  24686  recld2  24703  zdis  24705  opnreen  24720  cnheibor  24854  lebnumlem3  24862  nmoleub2lem3  25015  nmoleub2lem2  25016  nmoleub3  25019  ipcnlem2  25144  cmetcaulem  25188  nglmle  25202  cncmet  25222  csbren  25299  trirn  25300  minveclem4  25332  ovoliunlem1  25403  ovoliun2  25407  ovolscalem1  25414  ovolicopnf  25425  voliunlem2  25452  volsup  25457  ioorcl2  25473  uniiccvol  25481  uniioombllem4  25487  i1fd  25582  mbfi1fseqlem4  25619  itg2const2  25642  itg2eqa  25646  itg2split  25650  itg2i1fseqle  25655  itg2cnlem2  25663  dvcnv  25881  dveflem  25883  dvferm1lem  25888  dvlip2  25900  c1liplem1  25901  dvivthlem1  25913  lhop1lem  25918  dvcvx  25925  dvfsumle  25926  dvfsumleOLD  25927  dvfsumabs  25929  dvfsumlem4  25936  dvfsumrlim2  25939  ftc1a  25944  tdeglem4  25965  deg1pwle  26025  fta1blem  26076  aalioulem3  26242  aaliou2b  26249  ulmbdd  26307  ulmdvlem1  26309  itgulm  26317  pserdvlem2  26338  abelthlem3  26343  abelthlem5  26345  abelthlem6  26346  abelthlem7  26348  tanregt0  26448  argimlt0  26522  logdivlti  26529  logcnlem3  26553  logcnlem4  26554  logtayl  26569  logtayl2  26571  cxple2  26606  cxpcn3lem  26657  cxpaddle  26662  rtprmirr  26670  isosctrlem1  26728  atantayl  26847  efrlim  26879  efrlimOLD  26880  dfef2  26881  o1cxp  26885  cxp2lim  26887  divsqrtsumo1  26894  amgmlem  26900  logdifbnd  26904  emcllem7  26912  harmonicbnd4  26921  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamucov  26948  lgamcvg2  26965  gamcvg2  26970  ftalem2  26984  basellem2  26992  basellem5  26995  basellem9  26999  vma1  27076  sqff1o  27092  fsumfldivdiaglem  27099  chtub  27123  fsumvma2  27125  chpchtsum  27130  chpub  27131  logfaclbnd  27133  logfacbnd3  27134  logfacrlim  27135  logexprlim  27136  bcmono  27188  bposlem2  27196  bposlem5  27199  bposlem6  27200  lgsne0  27246  lgsquadlem1  27291  lgsquadlem2  27292  2sqblem  27342  2sqmod  27347  chebbnd1lem1  27380  chtppilimlem1  27384  chtppilimlem2  27385  chpchtlim  27390  rplogsumlem1  27395  dchrvmasumiflem1  27412  dchrisum0flblem2  27420  dchrisum0fno1  27422  dchrisum0lem2a  27428  dchrisum0lem3  27430  dirith  27440  mulog2sumlem1  27445  mulog2sumlem2  27446  log2sumbnd  27455  selberglem2  27457  logdivbnd  27467  selberg3lem1  27468  selberg4lem1  27471  pntrsumbnd2  27478  pntrlog2bndlem1  27488  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem3  27503  pntlemb  27508  pntlemn  27511  pntlemr  27513  pntlemj  27514  pntlemf  27516  pntlemo  27518  ostth2lem3  27546  ostth3  27549  addsuniflem  27908  sltp1d  27922  negsid  27947  negsunif  27961  mulsuniflem  28052  precsexlem9  28117  n0sge0  28230  zscut  28295  halfcut  28333  addhalfcut  28334  footeq  28651  hlperpnel  28652  perpdragALT  28654  perpdrag  28655  colperp  28656  mideulem2  28661  opphllem  28662  opphllem3  28676  lmieu  28711  trgcopy  28731  sacgr  28758  acopyeu  28761  usgredgleordALT  29161  eucrctshift  30172  nvabs  30601  smcnlem  30626  ubthlem2  30800  minvecolem4  30809  htthlem  30846  normpyc  31075  nmophmi  31960  hstle  32159  hstles  32160  stlei  32169  f1rnen  32553  nnmulge  32662  fsumiunle  32754  sgnmulsgn  32767  wrdt2ind  32875  xrge0npcan  32961  gsumwrd2dccat  33007  trsp2cyc  33080  archirngz  33143  archiabllem1a  33145  archiabllem2a  33148  archiabllem2c  33149  elrgspnlem1  33193  elrgspn  33197  elrgspnsubrunlem2  33199  ornglmulle  33283  orngrmulle  33284  rprmasso  33496  q1pdir  33568  r1pquslmic  33576  drngdimgt0  33614  lbsdiflsp0  33622  fldextrspundgle  33673  fldext2rspun  33677  minplyirredlem  33700  madjusmdetlem2  33818  esumpinfval  34063  esumpinfsum  34067  esumpcvgval  34068  esum2d  34083  esumiun  34084  dya2icoseg  34268  omssubadd  34291  carsgsigalem  34306  carsggect  34309  carsgclctunlem3  34311  omsmeas  34314  eulerpartlems  34351  signsplypnf  34541  signsply0  34542  reprlt  34610  reprinfz1  34613  hgt750lemc  34638  hgt750lemf  34644  pthhashvtx  35115  resconn  35233  sinccvglem  35659  circum  35661  btwnxfr  36044  nn0prpwlem  36310  dnibndlem2  36467  unblimceq0  36495  irrdiff  37314  poimirlem7  37621  mblfinlem3  37653  mblfinlem4  37654  itg2addnclem3  37667  ftc1anc  37695  isbnd3  37778  cntotbnd  37790  bfp  37818  rrndstprj2  37825  1cvrjat  39469  3atlem1  39477  3atlem6  39482  llnmlplnN  39533  2llnjaN  39560  2lplnja  39613  dalem57  39723  dalawlem11  39875  dalawlem12  39876  lhp2lt  39995  lhpj1  40016  lhpm0atN  40023  4atexlemex2  40065  lautm  40088  cdleme17b  40281  cdleme20j  40312  cdleme30a  40372  cdlemg4c  40606  cdlemg17a  40655  cdlemg31c  40693  trljco  40734  cdlemk46  40942  dia2dimlem2  41059  cdlemm10N  41112  cdlemn10  41200  dihmeetlem1N  41284  dihglblem5apreN  41285  dihmeetlem15N  41315  mapdat  41661  lcmineqlem19  42035  lcmineqlem20  42036  aks4d1p1p5  42063  aks4d1p8d2  42073  aks4d1p8  42075  aks4d1p9  42076  hashscontpow  42110  dvdsexpnn  42321  mullt0b1d  42471  selvvvval  42573  evlselv  42575  mhphflem  42584  fltnlta  42651  3cubeslem1  42672  irrapxlem1  42810  irrapxlem4  42813  pell1qrgaplem  42861  pellfundglb  42873  rmspecfund  42897  monotoddzzfi  42931  rmynn  42945  jm2.24nn  42948  jm2.17c  42951  jm2.24  42952  acongeq  42972  jm2.20nn  42986  jm2.26lem3  42990  jm2.27a  42994  jm2.27c  42996  rmydioph  43003  jm3.1lem2  43007  frlmpwfi  43087  areaquad  43205  cantnf2  43314  rp-isfinite6  43507  frege129d  43752  leeq1d  44146  imo72b2lem0  44154  imo72b2  44161  cvgdvgrat  44302  radcnvrat  44303  hashnzfzclim  44311  isosctrlem1ALT  44923  cncmpmax  45026  iooabslt  45497  fmul01lt1lem2  45583  clim1fr1  45599  limcrecl  45627  climxrrelem  45747  liminflbuz2  45813  dvnprodlem1  45944  stoweidlem1  45999  stoweidlem11  46009  stoweidlem14  46012  stoweidlem24  46022  stoweidlem26  46024  wallispilem4  46066  wallispilem5  46067  stirlinglem1  46072  fourierdlem51  46155  fourierdlem65  46169  fouriersw  46229  2leaddle2  47299  sqrtpwpw2p  47539  lighneallem4a  47609  flnn0div2ge  48522  logbpw2m1  48556  functermclem  49496  amgmwlem  49791