Theorem 3brtr4d 5118

Description: Substitution of equality into both sides of a binary relation. (Contributed by NM, 21-Feb-2005.)

Hypotheses

Ref	Expression
3brtr4d.1	⊢ (𝜑 → 𝐴𝑅𝐵)
3brtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3brtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3brtr4d	⊢ (𝜑 → 𝐶𝑅𝐷)

Proof of Theorem 3brtr4d

Step	Hyp	Ref	Expression
1		3brtr4d.1	. 2 ⊢ (𝜑 → 𝐴𝑅𝐵)
2		3brtr4d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
3		3brtr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	breq12d 5099	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087

This theorem is referenced by:  f1oiso2  7281  sucdom2  9107  ordtypelem6  9404  ttrcltr  9601  ttrclss  9605  ttrclselem2  9611  fin23lem26  10211  distrnq  10847  lediv12a  12010  recp1lt1  12015  ifle  13091  xleadd1a  13147  xlemul1a  13182  fldiv4p1lem1div2  13734  fldiv4lem1div2  13736  quoremz  13754  quoremnn0ALT  13756  intfracq  13758  modmulnn  13788  fzennn  13870  monoord2  13935  expgt1  14002  expmordi  14069  leexp2r  14076  leexp1a  14077  bernneq  14131  expmulnbnd  14137  digit1  14139  faclbnd  14192  faclbnd4lem3  14197  faclbnd4lem4  14198  faclbnd6  14201  facubnd  14202  hashdomi  14282  fzsdom2  14330  absrele  15210  absimle  15211  abstri  15233  abs2difabs  15237  limsupval2  15382  rlimrege0  15481  rlimrecl  15482  climsqz  15543  climsqz2  15544  rlimdiv  15548  rlimsqz  15552  rlimsqz2  15553  isercolllem1  15567  isercoll2  15571  fsumcvg2  15629  fsumrlim  15713  o1fsum  15715  cvgcmpce  15720  isumle  15746  climcndslem1  15751  climcndslem2  15752  harmonic  15761  expcnv  15766  explecnv  15767  geomulcvg  15778  efcllem  15979  ege2le3  15992  eflegeo  16025  rpnnen2lem4  16121  ruclem2  16136  ruclem8  16141  fsumdvds  16214  phibnd  16677  iserodd  16742  pcdvdstr  16783  pcprmpw2  16789  pockthg  16813  prmreclem4  16826  prmolefac  16953  2expltfac  16999  mod2ile  18395  pfxchn  18511  chnub  18523  chnccats1  18526  chnccat  18527  chnrev  18528  ex-chn2  18539  odsubdvds  19478  pgpfi  19512  fislw  19532  efgredlemd  19651  efgredlem  19654  frgpcpbl  19666  omndmul  20042  ogrpsub  20044  gsumle  20052  rnghmsubcsetc  20543  rhmsubcsetc  20572  rhmsubcrngc  20578  rhmsubc  20599  abvres  20741  abvtrivd  20742  znrrg  21497  ofldchr  21508  cstucnd  24193  psmetge0  24222  psmetres2  24224  xmetge0  24254  xmetres2  24271  imasf1oxmet  24285  comet  24423  stdbdxmet  24425  dscmet  24482  nrmmetd  24484  nmrtri  24534  tngngp  24564  nmolb2d  24628  nmoleub  24641  nmoco  24647  nmotri  24649  nmoid  24652  nmods  24654  cnmet  24681  xrsxmet  24720  metdstri  24762  metnrmlem3  24772  lebnumlem3  24884  ipcau2  25156  tcphcphlem1  25157  tcphcph  25159  trirn  25322  rrxmet  25330  rrxdstprj1  25331  minveclem2  25348  ovolunlem1a  25419  ovolscalem1  25436  volss  25456  voliunlem1  25473  volcn  25529  itg1climres  25637  mbfi1fseqlem5  25642  mbfi1fseqlem6  25643  itg2const2  25664  itg2seq  25665  itg2mulc  25670  itg2splitlem  25671  itg2monolem1  25673  itg2i1fseqle  25677  itg2i1fseq  25678  itg2i1fseq2  25679  itg2addlem  25681  itg2cnlem1  25684  itg2cnlem2  25685  iblss  25728  itgle  25733  ibladdlem  25743  iblabs  25752  iblabsr  25753  iblmulc2  25754  itgabs  25758  bddmulibl  25762  bddiblnc  25765  dvfsumabs  25951  dvfsumlem2  25955  dvfsumlem2OLD  25956  dvfsum2  25963  deg1suble  26034  deg1mul3le  26044  plyeq0lem  26137  dgrcolem2  26202  geolim3  26269  aaliou3lem2  26273  aaliou3lem8  26275  ulmdvlem1  26331  radcnvlem1  26344  radcnvlem2  26345  dvradcnv  26352  pserulm  26353  pserdvlem2  26360  abelthlem2  26364  abelthlem5  26367  abelthlem7  26370  abelth2  26374  tangtx  26436  tanabsge  26437  tanord1  26468  argregt0  26541  argrege0  26542  argimgt0  26543  abslogle  26549  logcnlem4  26576  logtayllem  26590  abscxpbnd  26685  ang180lem2  26742  atanlogsublem  26847  atans2  26863  leibpi  26874  birthdaylem3  26885  cxplim  26904  cxp2limlem  26908  cxploglim2  26911  jensenlem2  26920  jensen  26921  amgmlem  26922  emcllem2  26929  emcllem4  26931  emcllem7  26934  zetacvg  26947  lgamgulmlem2  26962  lgamgulmlem5  26965  ftalem5  27009  basellem4  27016  basellem6  27018  basellem8  27020  basellem9  27021  chtwordi  27088  chpwordi  27089  ppiwordi  27094  ppiub  27137  vmalelog  27138  chtlepsi  27139  chtleppi  27143  chtublem  27144  chtub  27145  chpub  27153  logfaclbnd  27155  logfacrlim  27157  dchrptlem3  27199  bcmono  27210  bclbnd  27213  bposlem1  27217  bposlem6  27222  bposlem9  27225  lgsqrlem4  27282  2lgslem1c  27326  chebbnd1lem1  27402  chebbnd1lem3  27404  chebbnd1  27405  chtppilimlem1  27406  vmadivsum  27415  rplogsumlem2  27418  dchrisumlema  27421  dchrisumlem3  27424  dchrmusum2  27427  dchrvmasumlem3  27432  dchrvmasumiflem1  27434  dchrisum0flblem1  27441  dchrisum0re  27446  dchrisum0lem2a  27450  mulogsumlem  27464  mulog2sumlem1  27467  mulog2sumlem2  27468  2vmadivsumlem  27473  selberg2lem  27483  selberg3lem1  27490  selberg4lem1  27493  pntrlog2bndlem3  27512  pntrlog2bndlem5  27514  pntrlog2bndlem6  27516  pntpbnd1  27519  pntlemc  27528  pntlemr  27535  pntlemk  27539  pntlemo  27540  abvcxp  27548  ostth2lem1  27551  padicabv  27563  ostth2lem2  27567  ostth2lem3  27568  ostth2lem4  27569  ostth2  27570  noextendlt  27603  noextendgt  27604  nosupbnd1  27648  nosupbnd2lem1  27649  noinfbnd1  27663  noinfbnd2lem1  27664  lltropt  27812  addsproplem2  27908  addsproplem4  27910  addsproplem5  27911  addsproplem6  27912  mulsproplem5  28054  mulsproplem6  28055  mulsproplem7  28056  mulsproplem8  28057  slemuld  28072  mulsuniflem  28083  slemul1ad  28116  precsexlem9  28148  legso  28572  trgcopy  28777  eucrct2eupth  30217  nvmtri  30643  imsmetlem  30662  vacn  30666  nmcvcn  30667  smcnlem  30669  blometi  30775  ipblnfi  30827  minvecolem2  30847  hhssnv  31236  nmcoplbi  32000  nmopcoi  32067  nmopcoadji  32073  idleop  32103  cdj1i  32405  isoun  32675  xlt2addrd  32734  nexple  32819  mgcf1o  32976  cycpmconjslem2  33116  archirngz  33150  elrgspnlem1  33201  q1pvsca  33556  lssdimle  33612  fedgmullem2  33635  fldextrspundglemul  33684  extdgfialglem1  33697  fldext2chn  33733  2sqr3minply  33785  cos9thpiminply  33793  pstmxmet  33902  esumpmono  34084  esumcvg  34091  meascnbl  34224  omsmon  34303  omsmeas  34328  dstfrvinc  34482  hgt750lemd  34653  hgt750lema  34662  hgt750leme  34663  swrdwlk  35163  derangenlem  35207  subfaclefac  35212  subfaclim  35224  erdszelem10  35236  sinccvglem  35708  iprodefisum  35777  unbdqndv2lem2  36544  itg2gt0cn  37715  ibladdnclem  37716  iblabsnc  37724  iblmulc2nc  37725  itgabsnc  37729  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  mettrifi  37797  equivbnd2  37832  heiborlem6  37856  bfplem1  37862  bfp  37864  rrnmet  37869  rrndstprj1  37870  rrndstprj2  37871  dalawlem3  39912  dalawlem4  39913  dalawlem6  39915  dalawlem9  39918  dalawlem11  39920  dalawlem12  39921  dalawlem15  39924  cdleme3c  40269  cdleme7e  40286  cdleme26e  40398  cdleme26eALTN  40400  cdleme27a  40406  cdleme32c  40482  cdleme32e  40484  cdleme32le  40486  cdlemg9b  40672  cdlemg12b  40683  cdlemg12d  40685  trlcolem  40765  trlcone  40767  cdlemk7  40887  cdlemk7u  40909  cdlemk39  40955  cdlemk11ta  40968  cdlemk11tc  40984  mapdcnvatN  41705  explt1d  42356  frlmvscadiccat  42539  3cubeslem1  42717  irrapxlem5  42859  pell1qrge1  42903  pell1qrgaplem  42906  pell14qrgapw  42909  pellqrex  42912  pellfund14  42931  jm2.17a  42993  jm2.17c  42995  acongeq  43016  jm2.19  43026  jm2.27a  43038  jm2.27c  43040  jm3.1lem2  43051  areaquad  43249  rp-isfinite6  43551  hashnzfzclim  44355  binomcxplemnotnn0  44389  absimlere  45517  monoord2xrv  45521  ltmod  45676  liminflelimsuplem  45813  dvbdfbdioolem2  45967  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  stoweidlem3  46041  stoweidlem26  46064  wallispilem1  46103  wallispilem5  46107  stirlinglem1  46112  stirlinglem5  46116  stirlinglem8  46119  stirlinglem10  46121  stirlinglem12  46123  fourierdlem6  46151  fourierdlem7  46152  fourierdlem14  46159  fourierdlem19  46164  fourierdlem35  46180  fourierdlem39  46184  fourierdlem42  46187  fourierdlem50  46194  fourierdlem73  46217  fourierdlem76  46220  fourierdlem77  46221  fourierdlem81  46225  fourierdlem90  46234  fourierdlem92  46236  fourierdlem93  46237  fourierdlem111  46255  fouriersw  46269  etransclem38  46310  sge0split  46447  ovnsslelem  46598  lighneallem4a  47639  rhmsubcALTV  48316  logbpw2m1  48599  dignn0flhalflem1  48647  dignn0flhalflem2  48648  1aryenef  48677  2aryenef  48688  2itscp  48813  amgmwlem  49834