Theorem 3brtr4d 5102

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  f1oiso2  7203  sucdom2  8822  ordtypelem6  9212  fin23lem26  10012  distrnq  10648  lediv12a  11798  recp1lt1  11803  ifle  12860  xleadd1a  12916  xlemul1a  12951  fldiv4p1lem1div2  13483  fldiv4lem1div2  13485  quoremz  13503  quoremnn0ALT  13505  intfracq  13507  modmulnn  13537  fzennn  13616  monoord2  13682  expgt1  13749  expmordi  13813  leexp2r  13820  leexp1a  13821  bernneq  13872  expmulnbnd  13878  digit1  13880  faclbnd  13932  faclbnd4lem3  13937  faclbnd4lem4  13938  faclbnd6  13941  facubnd  13942  hashdomi  14023  fzsdom2  14071  absrele  14948  absimle  14949  abstri  14970  abs2difabs  14974  limsupval2  15117  rlimrege0  15216  rlimrecl  15217  climsqz  15278  climsqz2  15279  rlimdiv  15285  rlimsqz  15289  rlimsqz2  15290  isercolllem1  15304  isercoll2  15308  fsumcvg2  15367  fsumrlim  15451  o1fsum  15453  cvgcmpce  15458  isumle  15484  climcndslem1  15489  climcndslem2  15490  harmonic  15499  expcnv  15504  explecnv  15505  geomulcvg  15516  efcllem  15715  ege2le3  15727  eflegeo  15758  rpnnen2lem4  15854  ruclem2  15869  ruclem8  15874  fsumdvds  15945  phibnd  16400  iserodd  16464  pcdvdstr  16505  pcprmpw2  16511  pockthg  16535  prmreclem4  16548  prmolefac  16675  2expltfac  16722  mod2ile  18127  odsubdvds  19091  pgpfi  19125  fislw  19145  efgredlemd  19265  efgredlem  19268  frgpcpbl  19280  abvres  20014  abvtrivd  20015  znrrg  20685  cstucnd  23344  psmetge0  23373  psmetres2  23375  xmetge0  23405  xmetres2  23422  imasf1oxmet  23436  comet  23575  stdbdxmet  23577  dscmet  23634  nrmmetd  23636  nmrtri  23686  tngngp  23724  nmolb2d  23788  nmoleub  23801  nmoco  23807  nmotri  23809  nmoid  23812  nmods  23814  cnmet  23841  xrsxmet  23878  metdstri  23920  metnrmlem3  23930  lebnumlem3  24032  ipcau2  24303  tcphcphlem1  24304  tcphcph  24306  trirn  24469  rrxmet  24477  rrxdstprj1  24478  minveclem2  24495  ovolunlem1a  24565  ovolscalem1  24582  volss  24602  voliunlem1  24619  volcn  24675  itg1climres  24784  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2const2  24811  itg2seq  24812  itg2mulc  24817  itg2splitlem  24818  itg2monolem1  24820  itg2i1fseqle  24824  itg2i1fseq  24825  itg2i1fseq2  24826  itg2addlem  24828  itg2cnlem1  24831  itg2cnlem2  24832  iblss  24874  itgle  24879  ibladdlem  24889  iblabs  24898  iblabsr  24899  iblmulc2  24900  itgabs  24904  bddmulibl  24908  bddiblnc  24911  dvfsumabs  25092  dvfsumlem2  25096  dvfsum2  25103  deg1suble  25177  deg1mul3le  25186  plyeq0lem  25276  dgrcolem2  25340  geolim3  25404  aaliou3lem2  25408  aaliou3lem8  25410  ulmdvlem1  25464  radcnvlem1  25477  radcnvlem2  25478  dvradcnv  25485  pserulm  25486  pserdvlem2  25492  abelthlem2  25496  abelthlem5  25499  abelthlem7  25502  abelth2  25506  tangtx  25567  tanabsge  25568  tanord1  25598  argregt0  25670  argrege0  25671  argimgt0  25672  abslogle  25678  logcnlem4  25705  logtayllem  25719  abscxpbnd  25811  ang180lem2  25865  atanlogsublem  25970  atans2  25986  leibpi  25997  birthdaylem3  26008  cxplim  26026  cxp2limlem  26030  cxploglim2  26033  jensenlem2  26042  jensen  26043  amgmlem  26044  emcllem2  26051  emcllem4  26053  emcllem7  26056  zetacvg  26069  lgamgulmlem2  26084  lgamgulmlem5  26087  ftalem5  26131  basellem4  26138  basellem6  26140  basellem8  26142  basellem9  26143  chtwordi  26210  chpwordi  26211  ppiwordi  26216  ppiub  26257  vmalelog  26258  chtlepsi  26259  chtleppi  26263  chtublem  26264  chtub  26265  chpub  26273  logfaclbnd  26275  logfacrlim  26277  dchrptlem3  26319  bcmono  26330  bclbnd  26333  bposlem1  26337  bposlem6  26342  bposlem9  26345  lgsqrlem4  26402  2lgslem1c  26446  chebbnd1lem1  26522  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  vmadivsum  26535  rplogsumlem2  26538  dchrisumlema  26541  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  dchrisum0re  26566  dchrisum0lem2a  26570  mulogsumlem  26584  mulog2sumlem1  26587  mulog2sumlem2  26588  2vmadivsumlem  26593  selberg2lem  26603  selberg3lem1  26610  selberg4lem1  26613  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntpbnd1  26639  pntlemc  26648  pntlemr  26655  pntlemk  26659  pntlemo  26660  abvcxp  26668  ostth2lem1  26671  padicabv  26683  ostth2lem2  26687  ostth2lem3  26688  ostth2lem4  26689  ostth2  26690  legso  26864  trgcopy  27069  eucrct2eupth  28510  nvmtri  28934  imsmetlem  28953  vacn  28957  nmcvcn  28958  smcnlem  28960  blometi  29066  ipblnfi  29118  minvecolem2  29138  hhssnv  29527  nmcoplbi  30291  nmopcoi  30358  nmopcoadji  30364  idleop  30394  cdj1i  30696  isoun  30936  xlt2addrd  30983  mgcf1o  31183  omndmul  31242  ogrpsub  31244  gsumle  31252  cycpmconjslem2  31324  archirngz  31345  ofldchr  31415  lssdimle  31593  fedgmullem2  31613  pstmxmet  31749  nexple  31877  esumpmono  31947  esumcvg  31954  meascnbl  32087  omsmon  32165  omsmeas  32190  dstfrvinc  32343  hgt750lemd  32528  hgt750lema  32537  hgt750leme  32538  swrdwlk  32988  derangenlem  33033  subfaclefac  33038  subfaclim  33050  erdszelem10  33062  sinccvglem  33530  iprodefisum  33613  ttrcltr  33702  ttrclss  33706  ttrclselem2  33712  noextendlt  33799  noextendgt  33800  nosupbnd1  33844  nosupbnd2lem1  33845  noinfbnd1  33859  noinfbnd2lem1  33860  unbdqndv2lem2  34617  itg2gt0cn  35759  ibladdnclem  35760  iblabsnc  35768  iblmulc2nc  35769  itgabsnc  35773  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  mettrifi  35842  equivbnd2  35877  heiborlem6  35901  bfplem1  35907  bfp  35909  rrnmet  35914  rrndstprj1  35915  rrndstprj2  35916  dalawlem3  37814  dalawlem4  37815  dalawlem6  37817  dalawlem9  37820  dalawlem11  37822  dalawlem12  37823  dalawlem15  37826  cdleme3c  38171  cdleme7e  38188  cdleme26e  38300  cdleme26eALTN  38302  cdleme27a  38308  cdleme32c  38384  cdleme32e  38386  cdleme32le  38388  cdlemg9b  38574  cdlemg12b  38585  cdlemg12d  38587  trlcolem  38667  trlcone  38669  cdlemk7  38789  cdlemk7u  38811  cdlemk39  38857  cdlemk11ta  38870  cdlemk11tc  38886  mapdcnvatN  39607  factwoffsmonot  40091  frlmvscadiccat  40163  3cubeslem1  40422  irrapxlem5  40564  pell1qrge1  40608  pell1qrgaplem  40611  pell14qrgapw  40614  pellqrex  40617  pellfund14  40636  jm2.17a  40698  jm2.17c  40700  acongeq  40721  jm2.19  40731  jm2.27a  40743  jm2.27c  40745  jm3.1lem2  40756  areaquad  40963  rp-isfinite6  41023  hashnzfzclim  41829  binomcxplemnotnn0  41863  absimlere  42910  monoord2xrv  42914  ltmod  43069  dvbdfbdioolem2  43360  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweidlem3  43434  stoweidlem26  43457  wallispilem1  43496  wallispilem5  43500  stirlinglem1  43505  stirlinglem5  43509  stirlinglem8  43512  stirlinglem10  43514  stirlinglem12  43516  fourierdlem6  43544  fourierdlem7  43545  fourierdlem14  43552  fourierdlem19  43557  fourierdlem35  43573  fourierdlem39  43577  fourierdlem42  43580  fourierdlem50  43587  fourierdlem73  43610  fourierdlem76  43613  fourierdlem77  43614  fourierdlem81  43618  fourierdlem90  43627  fourierdlem92  43629  fourierdlem93  43630  fourierdlem111  43648  fouriersw  43662  etransclem38  43703  sge0split  43837  lighneallem4a  44948  rnghmsubcsetc  45423  rhmsubcsetc  45469  rhmsubcrngc  45475  rhmsubc  45536  rhmsubcALTV  45554  logbpw2m1  45801  dignn0flhalflem1  45849  dignn0flhalflem2  45850  1aryenef  45879  2aryenef  45890  2itscp  46015  amgmwlem  46392