Theorem 3brtr4d 5139

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 5120	. 2 ⊢ (𝜑 → (𝐶𝑅𝐷 ↔ 𝐴𝑅𝐵))
5	1, 4	mpbird 257	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:  f1oiso2  7327  sucdom2  9167  ordtypelem6  9476  ttrcltr  9669  ttrclss  9673  ttrclselem2  9679  fin23lem26  10278  distrnq  10914  lediv12a  12076  recp1lt1  12081  ifle  13157  xleadd1a  13213  xlemul1a  13248  fldiv4p1lem1div2  13797  fldiv4lem1div2  13799  quoremz  13817  quoremnn0ALT  13819  intfracq  13821  modmulnn  13851  fzennn  13933  monoord2  13998  expgt1  14065  expmordi  14132  leexp2r  14139  leexp1a  14140  bernneq  14194  expmulnbnd  14200  digit1  14202  faclbnd  14255  faclbnd4lem3  14260  faclbnd4lem4  14261  faclbnd6  14264  facubnd  14265  hashdomi  14345  fzsdom2  14393  absrele  15274  absimle  15275  abstri  15297  abs2difabs  15301  limsupval2  15446  rlimrege0  15545  rlimrecl  15546  climsqz  15607  climsqz2  15608  rlimdiv  15612  rlimsqz  15616  rlimsqz2  15617  isercolllem1  15631  isercoll2  15635  fsumcvg2  15693  fsumrlim  15777  o1fsum  15779  cvgcmpce  15784  isumle  15810  climcndslem1  15815  climcndslem2  15816  harmonic  15825  expcnv  15830  explecnv  15831  geomulcvg  15842  efcllem  16043  ege2le3  16056  eflegeo  16089  rpnnen2lem4  16185  ruclem2  16200  ruclem8  16205  fsumdvds  16278  phibnd  16741  iserodd  16806  pcdvdstr  16847  pcprmpw2  16853  pockthg  16877  prmreclem4  16890  prmolefac  17017  2expltfac  17063  mod2ile  18453  odsubdvds  19501  pgpfi  19535  fislw  19555  efgredlemd  19674  efgredlem  19677  frgpcpbl  19689  rnghmsubcsetc  20542  rhmsubcsetc  20571  rhmsubcrngc  20577  rhmsubc  20598  abvres  20740  abvtrivd  20741  znrrg  21475  cstucnd  24171  psmetge0  24200  psmetres2  24202  xmetge0  24232  xmetres2  24249  imasf1oxmet  24263  comet  24401  stdbdxmet  24403  dscmet  24460  nrmmetd  24462  nmrtri  24512  tngngp  24542  nmolb2d  24606  nmoleub  24619  nmoco  24625  nmotri  24627  nmoid  24630  nmods  24632  cnmet  24659  xrsxmet  24698  metdstri  24740  metnrmlem3  24750  lebnumlem3  24862  ipcau2  25134  tcphcphlem1  25135  tcphcph  25137  trirn  25300  rrxmet  25308  rrxdstprj1  25309  minveclem2  25326  ovolunlem1a  25397  ovolscalem1  25414  volss  25434  voliunlem1  25451  volcn  25507  itg1climres  25615  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2const2  25642  itg2seq  25643  itg2mulc  25648  itg2splitlem  25649  itg2monolem1  25651  itg2i1fseqle  25655  itg2i1fseq  25656  itg2i1fseq2  25657  itg2addlem  25659  itg2cnlem1  25662  itg2cnlem2  25663  iblss  25706  itgle  25711  ibladdlem  25721  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgabs  25736  bddmulibl  25740  bddiblnc  25743  dvfsumabs  25929  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsum2  25941  deg1suble  26012  deg1mul3le  26022  plyeq0lem  26115  dgrcolem2  26180  geolim3  26247  aaliou3lem2  26251  aaliou3lem8  26253  ulmdvlem1  26309  radcnvlem1  26322  radcnvlem2  26323  dvradcnv  26330  pserulm  26331  pserdvlem2  26338  abelthlem2  26342  abelthlem5  26345  abelthlem7  26348  abelth2  26352  tangtx  26414  tanabsge  26415  tanord1  26446  argregt0  26519  argrege0  26520  argimgt0  26521  abslogle  26527  logcnlem4  26554  logtayllem  26568  abscxpbnd  26663  ang180lem2  26720  atanlogsublem  26825  atans2  26841  leibpi  26852  birthdaylem3  26863  cxplim  26882  cxp2limlem  26886  cxploglim2  26889  jensenlem2  26898  jensen  26899  amgmlem  26900  emcllem2  26907  emcllem4  26909  emcllem7  26912  zetacvg  26925  lgamgulmlem2  26940  lgamgulmlem5  26943  ftalem5  26987  basellem4  26994  basellem6  26996  basellem8  26998  basellem9  26999  chtwordi  27066  chpwordi  27067  ppiwordi  27072  ppiub  27115  vmalelog  27116  chtlepsi  27117  chtleppi  27121  chtublem  27122  chtub  27123  chpub  27131  logfaclbnd  27133  logfacrlim  27135  dchrptlem3  27177  bcmono  27188  bclbnd  27191  bposlem1  27195  bposlem6  27200  bposlem9  27203  lgsqrlem4  27260  2lgslem1c  27304  chebbnd1lem1  27380  chebbnd1lem3  27382  chebbnd1  27383  chtppilimlem1  27384  vmadivsum  27393  rplogsumlem2  27396  dchrisumlema  27399  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0re  27424  dchrisum0lem2a  27428  mulogsumlem  27442  mulog2sumlem1  27445  mulog2sumlem2  27446  2vmadivsumlem  27451  selberg2lem  27461  selberg3lem1  27468  selberg4lem1  27471  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntpbnd1  27497  pntlemc  27506  pntlemr  27513  pntlemk  27517  pntlemo  27518  abvcxp  27526  ostth2lem1  27529  padicabv  27541  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  ostth2  27548  noextendlt  27581  noextendgt  27582  nosupbnd1  27626  nosupbnd2lem1  27627  noinfbnd1  27641  noinfbnd2lem1  27642  lltropt  27784  addsproplem2  27877  addsproplem4  27879  addsproplem5  27880  addsproplem6  27881  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  slemuld  28041  mulsuniflem  28052  slemul1ad  28085  precsexlem9  28117  legso  28526  trgcopy  28731  eucrct2eupth  30174  nvmtri  30600  imsmetlem  30619  vacn  30623  nmcvcn  30624  smcnlem  30626  blometi  30732  ipblnfi  30784  minvecolem2  30804  hhssnv  31193  nmcoplbi  31957  nmopcoi  32024  nmopcoadji  32030  idleop  32060  cdj1i  32362  isoun  32625  xlt2addrd  32682  nexple  32769  mgcf1o  32929  pfxchn  32935  chnub  32938  chnccats1  32941  omndmul  33028  ogrpsub  33030  gsumle  33038  cycpmconjslem2  33112  archirngz  33143  elrgspnlem1  33193  ofldchr  33292  q1pvsca  33569  lssdimle  33603  fedgmullem2  33626  fldextrspundglemul  33674  fldext2chn  33718  2sqr3minply  33770  cos9thpiminply  33778  pstmxmet  33887  esumpmono  34069  esumcvg  34076  meascnbl  34209  omsmon  34289  omsmeas  34314  dstfrvinc  34468  hgt750lemd  34639  hgt750lema  34648  hgt750leme  34649  swrdwlk  35114  derangenlem  35158  subfaclefac  35163  subfaclim  35175  erdszelem10  35187  sinccvglem  35659  iprodefisum  35728  unbdqndv2lem2  36498  itg2gt0cn  37669  ibladdnclem  37670  iblabsnc  37678  iblmulc2nc  37679  itgabsnc  37683  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  mettrifi  37751  equivbnd2  37786  heiborlem6  37810  bfplem1  37816  bfp  37818  rrnmet  37823  rrndstprj1  37824  rrndstprj2  37825  dalawlem3  39867  dalawlem4  39868  dalawlem6  39870  dalawlem9  39873  dalawlem11  39875  dalawlem12  39876  dalawlem15  39879  cdleme3c  40224  cdleme7e  40241  cdleme26e  40353  cdleme26eALTN  40355  cdleme27a  40361  cdleme32c  40437  cdleme32e  40439  cdleme32le  40441  cdlemg9b  40627  cdlemg12b  40638  cdlemg12d  40640  trlcolem  40720  trlcone  40722  cdlemk7  40842  cdlemk7u  40864  cdlemk39  40910  cdlemk11ta  40923  cdlemk11tc  40939  mapdcnvatN  41660  explt1d  42311  frlmvscadiccat  42494  3cubeslem1  42672  irrapxlem5  42814  pell1qrge1  42858  pell1qrgaplem  42861  pell14qrgapw  42864  pellqrex  42867  pellfund14  42886  jm2.17a  42949  jm2.17c  42951  acongeq  42972  jm2.19  42982  jm2.27a  42994  jm2.27c  42996  jm3.1lem2  43007  areaquad  43205  rp-isfinite6  43507  hashnzfzclim  44311  binomcxplemnotnn0  44345  absimlere  45475  monoord2xrv  45479  ltmod  45636  liminflelimsuplem  45773  dvbdfbdioolem2  45927  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweidlem3  46001  stoweidlem26  46024  wallispilem1  46063  wallispilem5  46067  stirlinglem1  46072  stirlinglem5  46076  stirlinglem8  46079  stirlinglem10  46081  stirlinglem12  46083  fourierdlem6  46111  fourierdlem7  46112  fourierdlem14  46119  fourierdlem19  46124  fourierdlem35  46140  fourierdlem39  46144  fourierdlem42  46147  fourierdlem50  46154  fourierdlem73  46177  fourierdlem76  46180  fourierdlem77  46181  fourierdlem81  46185  fourierdlem90  46194  fourierdlem92  46196  fourierdlem93  46197  fourierdlem111  46215  fouriersw  46229  etransclem38  46270  sge0split  46407  ovnsslelem  46558  lighneallem4a  47609  rhmsubcALTV  48273  logbpw2m1  48556  dignn0flhalflem1  48604  dignn0flhalflem2  48605  1aryenef  48634  2aryenef  48645  2itscp  48770  amgmwlem  49791