Theorem eqbrtrrd 5137

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5111

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  dftpos4  8247  dif1en  9153  fodomfi  9279  fmptssfisupp  9361  cnfcom2lem  9677  dmttrcl  9697  ttrclselem2  9702  ficardadju  10199  enfin1ai  10383  pwcfsdom  10583  fpwwe2lem6  10636  fpwwe2  10643  canthp1lem1  10652  1nqenq  10962  prlem936  11047  lemulge11  12092  supaddc  12197  supmul1  12199  mul2lt0llt0  13138  mul2lt0lgt0  13139  xaddge0  13300  xadddi2  13339  ltexp2a  14220  leexp2a  14226  nnlesq  14259  digit1  14291  faclbnd4lem1  14347  faclbnd6  14353  facavg  14355  prsshashgt1  14465  nehash2  14529  sgnmulsgn  15170  abs3dif  15407  abs2dif  15408  limsupgre  15556  rlimclim1  15620  rlimuni  15625  rlimres2  15636  rlimcn1  15663  rlimcn1b  15664  recn2  15676  imcn2  15677  rlimo1  15692  o1rlimmul  15694  iserex  15732  isercoll  15743  caucvgrlem2  15750  caucvgr  15751  iseraltlem3  15759  summolem2a  15789  fsumge1  15872  o1fsum  15888  isumrpcl  15920  climcnds  15928  harmonic  15936  mertenslem1  15961  prodmolem2a  16011  ege2le3  16166  efgt1p2  16192  efgt1p  16193  eirrlem  16282  rpnnen2lem11  16302  fsumdvds  16388  bitsfzo  16515  bitsmod  16516  bitscmp  16518  mulgcd  16628  dvdssqlem  16646  nn0seqcvgd  16650  mulgcddvds  16735  rpdvds  16740  qden1elz  16838  phimullem  16860  hashgcdlem  16869  hashgcdeq  16871  pcdvdstr  16958  pockthg  16988  prmreclem1  16998  4sqlem11  17037  ramub1lem1  17108  ramub1lem2  17109  mreexexlem4d  17725  sscid  17903  latmlej21  18558  latmlej22  18559  lubel  18592  efginvrel1  19842  odadd2  19963  odadd  19964  gexexlem  19966  cyggex2  20011  ablfacrplem  20181  ablfac1c  20187  ablfac1eu  20189  pgpfac1lem3a  20192  isabvd  20965  ornglmulle  21020  orngrmulle  21021  mptscmfsuppd  21099  znrrg  21765  frlmphl  21981  frlmup1  21998  f1linds  22025  selvvvval  22343  psdmplcl  22375  chcoeffeqlem  23092  lmcn2  23857  metrtri  24565  imasdsf1olem  24581  stdbdxmet  24723  nrmmetd  24782  nmmtri  24830  nlmvscnlem2  24893  blcvx  25006  recld2  25023  zdis  25025  opnreen  25040  cnheibor  25165  lebnumlem3  25173  nmoleub2lem3  25325  nmoleub2lem2  25326  nmoleub3  25329  ipcnlem2  25454  cmetcaulem  25498  nglmle  25512  cncmet  25532  csbren  25609  trirn  25610  minveclem4  25642  ovoliunlem1  25712  ovoliun2  25716  ovolscalem1  25723  ovolicopnf  25734  voliunlem2  25761  volsup  25766  ioorcl2  25782  uniiccvol  25790  uniioombllem4  25796  i1fd  25891  mbfi1fseqlem4  25928  itg2const2  25951  itg2eqa  25955  itg2split  25959  itg2i1fseqle  25964  itg2cnlem2  25972  dvcnv  26187  dveflem  26189  dvferm1lem  26194  dvlip2  26205  c1liplem1  26206  dvivthlem1  26218  lhop1lem  26223  dvcvx  26230  dvfsumle  26231  dvfsumabs  26233  dvfsumlem4  26239  dvfsumrlim2  26242  ftc1a  26247  tdeglem4  26268  deg1pwle  26328  fta1blem  26379  aalioulem3  26548  aaliou2b  26555  ulmbdd  26612  ulmdvlem1  26614  itgulm  26622  pserdvlem2  26642  abelthlem3  26647  abelthlem5  26649  abelthlem6  26650  abelthlem7  26652  tanregt0  26755  argimlt0  26829  logdivlti  26836  logcnlem3  26860  logcnlem4  26861  logtayl  26876  logtayl2  26878  cxple2  26913  cxpcn3lem  26963  cxpaddle  26968  rtprmirr  26976  isosctrlem1  27034  atantayl  27153  efrlim  27185  dfef2  27186  o1cxp  27190  cxp2lim  27192  divsqrtsumo1  27199  amgmlem  27205  logdifbnd  27209  emcllem7  27217  harmonicbnd4  27226  fsumharmonic  27227  lgamgulmlem2  27245  lgamgulmlem3  27246  lgamucov  27253  lgamcvg2  27270  gamcvg2  27275  ftalem2  27289  basellem2  27297  basellem5  27300  basellem9  27304  vma1  27381  sqff1o  27397  fsumfldivdiaglem  27404  chtub  27427  fsumvma2  27429  chpchtsum  27434  chpub  27435  logfaclbnd  27437  logfacbnd3  27438  logfacrlim  27439  logexprlim  27440  bcmono  27492  bposlem2  27500  bposlem5  27503  bposlem6  27504  lgsne0  27550  lgsquadlem1  27595  lgsquadlem2  27596  2sqblem  27646  2sqmod  27651  chebbnd1lem1  27684  chtppilimlem1  27688  chtppilimlem2  27689  chpchtlim  27694  rplogsumlem1  27699  dchrvmasumiflem1  27716  dchrisum0flblem2  27724  dchrisum0fno1  27726  dchrisum0lem2a  27732  dchrisum0lem3  27734  dirith  27744  mulog2sumlem1  27749  mulog2sumlem2  27750  log2sumbnd  27759  selberglem2  27761  logdivbnd  27771  selberg3lem1  27772  selberg4lem1  27775  pntrsumbnd2  27782  pntrlog2bndlem1  27792  pntrlog2bndlem5  27796  pntrlog2bndlem6  27798  pntpbnd1a  27800  pntpbnd1  27801  pntpbnd2  27802  pntibndlem3  27807  pntlemb  27812  pntlemn  27815  pntlemr  27817  pntlemj  27818  pntlemf  27820  pntlemo  27822  ostth2lem3  27850  ostth3  27853  addsuniflem  28245  ltsp1d  28259  negsid  28285  negsunif  28299  negleft  28302  mulsuniflem  28393  precsexlem9  28459  n0sge0  28582  zcuts  28651  halfcut  28702  addhalfcut  28703  pw2cut2  28706  bdayfinbndlem1  28711  footeq  29055  hlperpnel  29057  perpdragALT  29059  perpdrag  29060  colperp  29061  mideulem2  29066  opphllem  29067  opphllem3  29081  lmieu  29144  trgcopy  29166  sacgr  29193  acopyeu  29196  perpeqlem  29201  perpprlng  29255  prlngmid2  29266  usgredgleordALT  29642  pthhashvtx  30142  eucrctshift  30665  nvabs  31095  smcnlem  31120  ubthlem2  31294  minvecolem4  31303  htthlem  31340  normpyc  31569  nmophmi  32454  hstle  32653  hstles  32654  stlei  32663  f1rnen  33044  nnmulge  33154  fsumiunle  33243  wrdt2ind  33339  xrge0npcan  33404  gsumwrd2dccat  33462  trsp2cyc  33507  archirngz  33573  archiabllem1a  33575  archiabllem2a  33578  archiabllem2c  33579  elrgspnlem1  33626  elrgspn  33630  elrgspnsubrunlem2  33632  rprmasso  33879  q1pdir  33957  r1pquslmic  33964  selvply1rhmlema  33972  selvply1rhmlem1  33974  evlextv  33996  mplvrpmga  33999  mplvrpmrhm  34001  drngdimgt0  34072  lbsdiflsp0  34080  fldextrspundgle  34132  fldext2rspun  34136  minplyirredlem  34164  madjusmdetlem2  34282  esumpinfval  34527  esumpinfsum  34531  esumpcvgval  34532  esum2d  34547  esumiun  34548  dya2icoseg  34732  omssubadd  34755  carsgsigalem  34770  carsggect  34773  carsgclctunlem3  34775  omsmeas  34778  eulerpartlems  34815  signsplypnf  35002  signsply0  35003  reprlt  35071  reprinfz1  35074  hgt750lemc  35099  hgt750lemf  35105  resconn  35775  sinccvglem  36201  circum  36203  btwnxfr  36585  nn0prpwlem  36890  dnibndlem2  37125  unblimceq0  37153  irrdiff  38027  poimirlem7  38335  mblfinlem3  38367  mblfinlem4  38368  itg2addnclem3  38381  ftc1anc  38409  isbnd3  38493  cntotbnd  38505  bfp  38533  rrndstprj2  38540  1cvrjat  40307  3atlem1  40315  3atlem6  40320  llnmlplnN  40371  2llnjaN  40398  2lplnja  40451  dalem57  40561  dalawlem11  40713  dalawlem12  40714  lhp2lt  40833  lhpj1  40854  lhpm0atN  40861  4atexlemex2  40903  lautm  40926  cdleme17b  41119  cdleme20j  41150  cdleme30a  41210  cdlemg4c  41444  cdlemg17a  41493  cdlemg31c  41531  trljco  41572  cdlemk46  41780  dia2dimlem2  41897  cdlemm10N  41950  cdlemn10  42038  dihmeetlem1N  42122  dihglblem5apreN  42123  dihmeetlem15N  42153  mapdat  42499  lcmineqlem19  42872  lcmineqlem20  42873  aks4d1p1p5  42900  aks4d1p8d2  42910  aks4d1p8  42912  aks4d1p9  42913  hashscontpow  42947  dvdsexpnn  43152  mullt0b1d  43315  evlselv  43379  mhphflem  43386  fltnlta  43453  3cubeslem1  43473  irrapxlem1  43607  irrapxlem4  43610  pell1qrgaplem  43658  pellfundglb  43670  rmspecfund  43694  monotoddzzfi  43727  rmynn  43741  jm2.24nn  43744  jm2.17c  43747  jm2.24  43748  acongeq  43768  jm2.20nn  43782  jm2.26lem3  43786  jm2.27a  43790  jm2.27c  43792  rmydioph  43799  jm3.1lem2  43803  frlmpwfi  43883  areaquad  44001  cantnf2  44110  rp-isfinite6  44302  frege129d  44547  leeq1d  44941  imo72b2lem0  44949  imo72b2  44956  cvgdvgrat  45081  radcnvrat  45082  hashnzfzclim  45090  isosctrlem1ALT  45700  cncmpmax  45810  iooabslt  46273  fmul01lt1lem2  46359  clim1fr1  46375  limcrecl  46403  climxrrelem  46521  liminflbuz2  46587  dvnprodlem1  46718  stoweidlem1  46773  stoweidlem11  46783  stoweidlem14  46786  stoweidlem24  46796  stoweidlem26  46798  wallispilem4  46840  wallispilem5  46841  stirlinglem1  46846  fourierdlem51  46929  fourierdlem65  46943  fouriersw  47003  2leaddle2  48093  2timesltsqm1  48174  sqrtpwpw2p  48348  lighneallem4a  48418  flnn0div2ge  49370  logbpw2m1  49404  functermclem  50342  amgmwlem  50707