Theorem 3brtr4d 5175

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144

This theorem is referenced by:  f1oiso2  7372  sucdom2OLD  9122  sucdom2  9243  ordtypelem6  9563  ttrcltr  9756  ttrclss  9760  ttrclselem2  9766  fin23lem26  10365  distrnq  11001  lediv12a  12161  recp1lt1  12166  ifle  13239  xleadd1a  13295  xlemul1a  13330  fldiv4p1lem1div2  13875  fldiv4lem1div2  13877  quoremz  13895  quoremnn0ALT  13897  intfracq  13899  modmulnn  13929  fzennn  14009  monoord2  14074  expgt1  14141  expmordi  14207  leexp2r  14214  leexp1a  14215  bernneq  14268  expmulnbnd  14274  digit1  14276  faclbnd  14329  faclbnd4lem3  14334  faclbnd4lem4  14335  faclbnd6  14338  facubnd  14339  hashdomi  14419  fzsdom2  14467  absrele  15347  absimle  15348  abstri  15369  abs2difabs  15373  limsupval2  15516  rlimrege0  15615  rlimrecl  15616  climsqz  15677  climsqz2  15678  rlimdiv  15682  rlimsqz  15686  rlimsqz2  15687  isercolllem1  15701  isercoll2  15705  fsumcvg2  15763  fsumrlim  15847  o1fsum  15849  cvgcmpce  15854  isumle  15880  climcndslem1  15885  climcndslem2  15886  harmonic  15895  expcnv  15900  explecnv  15901  geomulcvg  15912  efcllem  16113  ege2le3  16126  eflegeo  16157  rpnnen2lem4  16253  ruclem2  16268  ruclem8  16273  fsumdvds  16345  phibnd  16808  iserodd  16873  pcdvdstr  16914  pcprmpw2  16920  pockthg  16944  prmreclem4  16957  prmolefac  17084  2expltfac  17130  mod2ile  18539  odsubdvds  19589  pgpfi  19623  fislw  19643  efgredlemd  19762  efgredlem  19765  frgpcpbl  19777  rnghmsubcsetc  20633  rhmsubcsetc  20662  rhmsubcrngc  20668  rhmsubc  20689  abvres  20832  abvtrivd  20833  znrrg  21584  cstucnd  24293  psmetge0  24322  psmetres2  24324  xmetge0  24354  xmetres2  24371  imasf1oxmet  24385  comet  24526  stdbdxmet  24528  dscmet  24585  nrmmetd  24587  nmrtri  24637  tngngp  24675  nmolb2d  24739  nmoleub  24752  nmoco  24758  nmotri  24760  nmoid  24763  nmods  24765  cnmet  24792  xrsxmet  24831  metdstri  24873  metnrmlem3  24883  lebnumlem3  24995  ipcau2  25268  tcphcphlem1  25269  tcphcph  25271  trirn  25434  rrxmet  25442  rrxdstprj1  25443  minveclem2  25460  ovolunlem1a  25531  ovolscalem1  25548  volss  25568  voliunlem1  25585  volcn  25641  itg1climres  25749  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  itg2const2  25776  itg2seq  25777  itg2mulc  25782  itg2splitlem  25783  itg2monolem1  25785  itg2i1fseqle  25789  itg2i1fseq  25790  itg2i1fseq2  25791  itg2addlem  25793  itg2cnlem1  25796  itg2cnlem2  25797  iblss  25840  itgle  25845  ibladdlem  25855  iblabs  25864  iblabsr  25865  iblmulc2  25866  itgabs  25870  bddmulibl  25874  bddiblnc  25877  dvfsumabs  26063  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsum2  26075  deg1suble  26146  deg1mul3le  26156  plyeq0lem  26249  dgrcolem2  26314  geolim3  26381  aaliou3lem2  26385  aaliou3lem8  26387  ulmdvlem1  26443  radcnvlem1  26456  radcnvlem2  26457  dvradcnv  26464  pserulm  26465  pserdvlem2  26472  abelthlem2  26476  abelthlem5  26479  abelthlem7  26482  abelth2  26486  tangtx  26547  tanabsge  26548  tanord1  26579  argregt0  26652  argrege0  26653  argimgt0  26654  abslogle  26660  logcnlem4  26687  logtayllem  26701  abscxpbnd  26796  ang180lem2  26853  atanlogsublem  26958  atans2  26974  leibpi  26985  birthdaylem3  26996  cxplim  27015  cxp2limlem  27019  cxploglim2  27022  jensenlem2  27031  jensen  27032  amgmlem  27033  emcllem2  27040  emcllem4  27042  emcllem7  27045  zetacvg  27058  lgamgulmlem2  27073  lgamgulmlem5  27076  ftalem5  27120  basellem4  27127  basellem6  27129  basellem8  27131  basellem9  27132  chtwordi  27199  chpwordi  27200  ppiwordi  27205  ppiub  27248  vmalelog  27249  chtlepsi  27250  chtleppi  27254  chtublem  27255  chtub  27256  chpub  27264  logfaclbnd  27266  logfacrlim  27268  dchrptlem3  27310  bcmono  27321  bclbnd  27324  bposlem1  27328  bposlem6  27333  bposlem9  27336  lgsqrlem4  27393  2lgslem1c  27437  chebbnd1lem1  27513  chebbnd1lem3  27515  chebbnd1  27516  chtppilimlem1  27517  vmadivsum  27526  rplogsumlem2  27529  dchrisumlema  27532  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrisum0flblem1  27552  dchrisum0re  27557  dchrisum0lem2a  27561  mulogsumlem  27575  mulog2sumlem1  27578  mulog2sumlem2  27579  2vmadivsumlem  27584  selberg2lem  27594  selberg3lem1  27601  selberg4lem1  27604  pntrlog2bndlem3  27623  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntpbnd1  27630  pntlemc  27639  pntlemr  27646  pntlemk  27650  pntlemo  27651  abvcxp  27659  ostth2lem1  27662  padicabv  27674  ostth2lem2  27678  ostth2lem3  27679  ostth2lem4  27680  ostth2  27681  noextendlt  27714  noextendgt  27715  nosupbnd1  27759  nosupbnd2lem1  27760  noinfbnd1  27774  noinfbnd2lem1  27775  lltropt  27911  addsproplem2  28003  addsproplem4  28005  addsproplem5  28006  addsproplem6  28007  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  slemuld  28164  mulsuniflem  28175  slemul1ad  28208  precsexlem9  28239  legso  28607  trgcopy  28812  eucrct2eupth  30264  nvmtri  30690  imsmetlem  30709  vacn  30713  nmcvcn  30714  smcnlem  30716  blometi  30822  ipblnfi  30874  minvecolem2  30894  hhssnv  31283  nmcoplbi  32047  nmopcoi  32114  nmopcoadji  32120  idleop  32150  cdj1i  32452  isoun  32711  xlt2addrd  32762  nexple  32833  mgcf1o  32993  pfxchn  32999  chnub  33002  chnccats1  33005  omndmul  33091  ogrpsub  33093  gsumle  33101  cycpmconjslem2  33175  archirngz  33196  elrgspnlem1  33246  ofldchr  33344  q1pvsca  33624  lssdimle  33658  fedgmullem2  33681  fldextrspundglemul  33729  fldext2chn  33769  2sqr3minply  33791  pstmxmet  33896  esumpmono  34080  esumcvg  34087  meascnbl  34220  omsmon  34300  omsmeas  34325  dstfrvinc  34479  hgt750lemd  34663  hgt750lema  34672  hgt750leme  34673  swrdwlk  35132  derangenlem  35176  subfaclefac  35181  subfaclim  35193  erdszelem10  35205  sinccvglem  35677  iprodefisum  35741  unbdqndv2lem2  36511  itg2gt0cn  37682  ibladdnclem  37683  iblabsnc  37691  iblmulc2nc  37692  itgabsnc  37696  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  mettrifi  37764  equivbnd2  37799  heiborlem6  37823  bfplem1  37829  bfp  37831  rrnmet  37836  rrndstprj1  37837  rrndstprj2  37838  dalawlem3  39875  dalawlem4  39876  dalawlem6  39878  dalawlem9  39881  dalawlem11  39883  dalawlem12  39884  dalawlem15  39887  cdleme3c  40232  cdleme7e  40249  cdleme26e  40361  cdleme26eALTN  40363  cdleme27a  40369  cdleme32c  40445  cdleme32e  40447  cdleme32le  40449  cdlemg9b  40635  cdlemg12b  40646  cdlemg12d  40648  trlcolem  40728  trlcone  40730  cdlemk7  40850  cdlemk7u  40872  cdlemk39  40918  cdlemk11ta  40931  cdlemk11tc  40947  mapdcnvatN  41668  factwoffsmonot  42243  explt1d  42358  frlmvscadiccat  42516  3cubeslem1  42695  irrapxlem5  42837  pell1qrge1  42881  pell1qrgaplem  42884  pell14qrgapw  42887  pellqrex  42890  pellfund14  42909  jm2.17a  42972  jm2.17c  42974  acongeq  42995  jm2.19  43005  jm2.27a  43017  jm2.27c  43019  jm3.1lem2  43030  areaquad  43228  rp-isfinite6  43531  hashnzfzclim  44341  binomcxplemnotnn0  44375  absimlere  45490  monoord2xrv  45494  ltmod  45653  dvbdfbdioolem2  45944  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweidlem3  46018  stoweidlem26  46041  wallispilem1  46080  wallispilem5  46084  stirlinglem1  46089  stirlinglem5  46093  stirlinglem8  46096  stirlinglem10  46098  stirlinglem12  46100  fourierdlem6  46128  fourierdlem7  46129  fourierdlem14  46136  fourierdlem19  46141  fourierdlem35  46157  fourierdlem39  46161  fourierdlem42  46164  fourierdlem50  46171  fourierdlem73  46194  fourierdlem76  46197  fourierdlem77  46198  fourierdlem81  46202  fourierdlem90  46211  fourierdlem92  46213  fourierdlem93  46214  fourierdlem111  46232  fouriersw  46246  etransclem38  46287  sge0split  46424  ovnsslelem  46575  lighneallem4a  47595  rhmsubcALTV  48201  logbpw2m1  48488  dignn0flhalflem1  48536  dignn0flhalflem2  48537  1aryenef  48566  2aryenef  48577  2itscp  48702  amgmwlem  49321