Theorem 3brtr4d 5132

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 5113	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 257	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

Syntax hints:   → wi 4   = wceq 1542   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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  f1oiso2  7308  sucdom2  9139  ordtypelem6  9440  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  fin23lem26  10247  distrnq  10884  lediv12a  12047  recp1lt1  12052  ifle  13124  xleadd1a  13180  xlemul1a  13215  fldiv4p1lem1div2  13767  fldiv4lem1div2  13769  quoremz  13787  quoremnn0ALT  13789  intfracq  13791  modmulnn  13821  fzennn  13903  monoord2  13968  expgt1  14035  expmordi  14102  leexp2r  14109  leexp1a  14110  bernneq  14164  expmulnbnd  14170  digit1  14172  faclbnd  14225  faclbnd4lem3  14230  faclbnd4lem4  14231  faclbnd6  14234  facubnd  14235  hashdomi  14315  fzsdom2  14363  absrele  15243  absimle  15244  abstri  15266  abs2difabs  15270  limsupval2  15415  rlimrege0  15514  rlimrecl  15515  climsqz  15576  climsqz2  15577  rlimdiv  15581  rlimsqz  15585  rlimsqz2  15586  isercolllem1  15600  isercoll2  15604  fsumcvg2  15662  fsumrlim  15746  o1fsum  15748  cvgcmpce  15753  isumle  15779  climcndslem1  15784  climcndslem2  15785  harmonic  15794  expcnv  15799  explecnv  15800  geomulcvg  15811  efcllem  16012  ege2le3  16025  eflegeo  16058  rpnnen2lem4  16154  ruclem2  16169  ruclem8  16174  fsumdvds  16247  phibnd  16710  iserodd  16775  pcdvdstr  16816  pcprmpw2  16822  pockthg  16846  prmreclem4  16859  prmolefac  16986  2expltfac  17032  mod2ile  18429  pfxchn  18545  chnub  18557  chnccats1  18560  chnccat  18561  chnrev  18562  ex-chn2  18573  odsubdvds  19512  pgpfi  19546  fislw  19566  efgredlemd  19685  efgredlem  19688  frgpcpbl  19700  omndmul  20076  ogrpsub  20078  gsumle  20086  rnghmsubcsetc  20578  rhmsubcsetc  20607  rhmsubcrngc  20613  rhmsubc  20634  abvres  20776  abvtrivd  20777  znrrg  21532  ofldchr  21543  cstucnd  24239  psmetge0  24268  psmetres2  24270  xmetge0  24300  xmetres2  24317  imasf1oxmet  24331  comet  24469  stdbdxmet  24471  dscmet  24528  nrmmetd  24530  nmrtri  24580  tngngp  24610  nmolb2d  24674  nmoleub  24687  nmoco  24693  nmotri  24695  nmoid  24698  nmods  24700  cnmet  24727  xrsxmet  24766  metdstri  24808  metnrmlem3  24818  lebnumlem3  24930  ipcau2  25202  tcphcphlem1  25203  tcphcph  25205  trirn  25368  rrxmet  25376  rrxdstprj1  25377  minveclem2  25394  ovolunlem1a  25465  ovolscalem1  25482  volss  25502  voliunlem1  25519  volcn  25575  itg1climres  25683  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  itg2const2  25710  itg2seq  25711  itg2mulc  25716  itg2splitlem  25717  itg2monolem1  25719  itg2i1fseqle  25723  itg2i1fseq  25724  itg2i1fseq2  25725  itg2addlem  25727  itg2cnlem1  25730  itg2cnlem2  25731  iblss  25774  itgle  25779  ibladdlem  25789  iblabs  25798  iblabsr  25799  iblmulc2  25800  itgabs  25804  bddmulibl  25808  bddiblnc  25811  dvfsumabs  25997  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsum2  26009  deg1suble  26080  deg1mul3le  26090  plyeq0lem  26183  dgrcolem2  26248  geolim3  26315  aaliou3lem2  26319  aaliou3lem8  26321  ulmdvlem1  26377  radcnvlem1  26390  radcnvlem2  26391  dvradcnv  26398  pserulm  26399  pserdvlem2  26406  abelthlem2  26410  abelthlem5  26413  abelthlem7  26416  abelth2  26420  tangtx  26482  tanabsge  26483  tanord1  26514  argregt0  26587  argrege0  26588  argimgt0  26589  abslogle  26595  logcnlem4  26622  logtayllem  26636  abscxpbnd  26731  ang180lem2  26788  atanlogsublem  26893  atans2  26909  leibpi  26920  birthdaylem3  26931  cxplim  26950  cxp2limlem  26954  cxploglim2  26957  jensenlem2  26966  jensen  26967  amgmlem  26968  emcllem2  26975  emcllem4  26977  emcllem7  26980  zetacvg  26993  lgamgulmlem2  27008  lgamgulmlem5  27011  ftalem5  27055  basellem4  27062  basellem6  27064  basellem8  27066  basellem9  27067  chtwordi  27134  chpwordi  27135  ppiwordi  27140  ppiub  27183  vmalelog  27184  chtlepsi  27185  chtleppi  27189  chtublem  27190  chtub  27191  chpub  27199  logfaclbnd  27201  logfacrlim  27203  dchrptlem3  27245  bcmono  27256  bclbnd  27259  bposlem1  27263  bposlem6  27268  bposlem9  27271  lgsqrlem4  27328  2lgslem1c  27372  chebbnd1lem1  27448  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  vmadivsum  27461  rplogsumlem2  27464  dchrisumlema  27467  dchrisumlem3  27470  dchrmusum2  27473  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  dchrisum0re  27492  dchrisum0lem2a  27496  mulogsumlem  27510  mulog2sumlem1  27513  mulog2sumlem2  27514  2vmadivsumlem  27519  selberg2lem  27529  selberg3lem1  27536  selberg4lem1  27539  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntpbnd1  27565  pntlemc  27574  pntlemr  27581  pntlemk  27585  pntlemo  27586  abvcxp  27594  ostth2lem1  27597  padicabv  27609  ostth2lem2  27613  ostth2lem3  27614  ostth2lem4  27615  ostth2  27616  noextendlt  27649  noextendgt  27650  nosupbnd1  27694  nosupbnd2lem1  27695  noinfbnd1  27709  noinfbnd2lem1  27710  lltr  27870  addsproplem2  27978  addsproplem4  27980  addsproplem5  27981  addsproplem6  27982  mulsproplem5  28128  mulsproplem6  28129  mulsproplem7  28130  mulsproplem8  28131  lemulsd  28146  mulsuniflem  28157  lemuls1ad  28190  precsexlem9  28223  bdaypw2n0bndlem  28471  legso  28683  trgcopy  28888  eucrct2eupth  30332  nvmtri  30759  imsmetlem  30778  vacn  30782  nmcvcn  30783  smcnlem  30785  blometi  30891  ipblnfi  30943  minvecolem2  30963  hhssnv  31352  nmcoplbi  32116  nmopcoi  32183  nmopcoadji  32189  idleop  32219  cdj1i  32521  isoun  32792  xlt2addrd  32850  nexple  32936  mgcf1o  33096  cycpmconjslem2  33249  archirngz  33283  elrgspnlem1  33336  q1pvsca  33697  lssdimle  33785  fedgmullem2  33808  fldextrspundglemul  33857  extdgfialglem1  33870  fldext2chn  33906  2sqr3minply  33958  cos9thpiminply  33966  pstmxmet  34075  esumpmono  34257  esumcvg  34264  meascnbl  34397  omsmon  34476  omsmeas  34501  dstfrvinc  34655  hgt750lemd  34826  hgt750lema  34835  hgt750leme  34836  swrdwlk  35343  derangenlem  35387  subfaclefac  35392  subfaclim  35404  erdszelem10  35416  sinccvglem  35888  iprodefisum  35957  unbdqndv2lem2  36732  itg2gt0cn  37926  ibladdnclem  37927  iblabsnc  37935  iblmulc2nc  37936  itgabsnc  37940  ftc1anclem7  37950  ftc1anclem8  37951  ftc1anc  37952  mettrifi  38008  equivbnd2  38043  heiborlem6  38067  bfplem1  38073  bfp  38075  rrnmet  38080  rrndstprj1  38081  rrndstprj2  38082  dalawlem3  40249  dalawlem4  40250  dalawlem6  40252  dalawlem9  40255  dalawlem11  40257  dalawlem12  40258  dalawlem15  40261  cdleme3c  40606  cdleme7e  40623  cdleme26e  40735  cdleme26eALTN  40737  cdleme27a  40743  cdleme32c  40819  cdleme32e  40821  cdleme32le  40823  cdlemg9b  41009  cdlemg12b  41020  cdlemg12d  41022  trlcolem  41102  trlcone  41104  cdlemk7  41224  cdlemk7u  41246  cdlemk39  41292  cdlemk11ta  41305  cdlemk11tc  41321  mapdcnvatN  42042  explt1d  42693  frlmvscadiccat  42876  3cubeslem1  43041  irrapxlem5  43183  pell1qrge1  43227  pell1qrgaplem  43230  pell14qrgapw  43233  pellqrex  43236  pellfund14  43255  jm2.17a  43317  jm2.17c  43319  acongeq  43340  jm2.19  43350  jm2.27a  43362  jm2.27c  43364  jm3.1lem2  43375  areaquad  43573  rp-isfinite6  43874  hashnzfzclim  44678  binomcxplemnotnn0  44712  absimlere  45837  monoord2xrv  45841  ltmod  45996  liminflelimsuplem  46133  dvbdfbdioolem2  46287  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  stoweidlem3  46361  stoweidlem26  46384  wallispilem1  46423  wallispilem5  46427  stirlinglem1  46432  stirlinglem5  46436  stirlinglem8  46439  stirlinglem10  46441  stirlinglem12  46443  fourierdlem6  46471  fourierdlem7  46472  fourierdlem14  46479  fourierdlem19  46484  fourierdlem35  46500  fourierdlem39  46504  fourierdlem42  46507  fourierdlem50  46514  fourierdlem73  46537  fourierdlem76  46540  fourierdlem77  46541  fourierdlem81  46545  fourierdlem90  46554  fourierdlem92  46556  fourierdlem93  46557  fourierdlem111  46575  fouriersw  46589  etransclem38  46630  sge0split  46767  ovnsslelem  46918  chnsubseq  47238  chnsuslle  47239  chnerlem1  47240  lighneallem4a  47968  rhmsubcALTV  48645  logbpw2m1  48927  dignn0flhalflem1  48975  dignn0flhalflem2  48976  1aryenef  49005  2aryenef  49016  2itscp  49141  amgmwlem  50161