Theorem 3brtr4d 5107

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  f1oiso2  7232  sucdom2OLD  8878  sucdom2  8998  ordtypelem6  9291  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  fin23lem26  10090  distrnq  10726  lediv12a  11877  recp1lt1  11882  ifle  12940  xleadd1a  12996  xlemul1a  13031  fldiv4p1lem1div2  13564  fldiv4lem1div2  13566  quoremz  13584  quoremnn0ALT  13586  intfracq  13588  modmulnn  13618  fzennn  13697  monoord2  13763  expgt1  13830  expmordi  13894  leexp2r  13901  leexp1a  13902  bernneq  13953  expmulnbnd  13959  digit1  13961  faclbnd  14013  faclbnd4lem3  14018  faclbnd4lem4  14019  faclbnd6  14022  facubnd  14023  hashdomi  14104  fzsdom2  14152  absrele  15029  absimle  15030  abstri  15051  abs2difabs  15055  limsupval2  15198  rlimrege0  15297  rlimrecl  15298  climsqz  15359  climsqz2  15360  rlimdiv  15366  rlimsqz  15370  rlimsqz2  15371  isercolllem1  15385  isercoll2  15389  fsumcvg2  15448  fsumrlim  15532  o1fsum  15534  cvgcmpce  15539  isumle  15565  climcndslem1  15570  climcndslem2  15571  harmonic  15580  expcnv  15585  explecnv  15586  geomulcvg  15597  efcllem  15796  ege2le3  15808  eflegeo  15839  rpnnen2lem4  15935  ruclem2  15950  ruclem8  15955  fsumdvds  16026  phibnd  16481  iserodd  16545  pcdvdstr  16586  pcprmpw2  16592  pockthg  16616  prmreclem4  16629  prmolefac  16756  2expltfac  16803  mod2ile  18221  odsubdvds  19185  pgpfi  19219  fislw  19239  efgredlemd  19359  efgredlem  19362  frgpcpbl  19374  abvres  20108  abvtrivd  20109  znrrg  20782  cstucnd  23445  psmetge0  23474  psmetres2  23476  xmetge0  23506  xmetres2  23523  imasf1oxmet  23537  comet  23678  stdbdxmet  23680  dscmet  23737  nrmmetd  23739  nmrtri  23789  tngngp  23827  nmolb2d  23891  nmoleub  23904  nmoco  23910  nmotri  23912  nmoid  23915  nmods  23917  cnmet  23944  xrsxmet  23981  metdstri  24023  metnrmlem3  24033  lebnumlem3  24135  ipcau2  24407  tcphcphlem1  24408  tcphcph  24410  trirn  24573  rrxmet  24581  rrxdstprj1  24582  minveclem2  24599  ovolunlem1a  24669  ovolscalem1  24686  volss  24706  voliunlem1  24723  volcn  24779  itg1climres  24888  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  itg2const2  24915  itg2seq  24916  itg2mulc  24921  itg2splitlem  24922  itg2monolem1  24924  itg2i1fseqle  24928  itg2i1fseq  24929  itg2i1fseq2  24930  itg2addlem  24932  itg2cnlem1  24935  itg2cnlem2  24936  iblss  24978  itgle  24983  ibladdlem  24993  iblabs  25002  iblabsr  25003  iblmulc2  25004  itgabs  25008  bddmulibl  25012  bddiblnc  25015  dvfsumabs  25196  dvfsumlem2  25200  dvfsum2  25207  deg1suble  25281  deg1mul3le  25290  plyeq0lem  25380  dgrcolem2  25444  geolim3  25508  aaliou3lem2  25512  aaliou3lem8  25514  ulmdvlem1  25568  radcnvlem1  25581  radcnvlem2  25582  dvradcnv  25589  pserulm  25590  pserdvlem2  25596  abelthlem2  25600  abelthlem5  25603  abelthlem7  25606  abelth2  25610  tangtx  25671  tanabsge  25672  tanord1  25702  argregt0  25774  argrege0  25775  argimgt0  25776  abslogle  25782  logcnlem4  25809  logtayllem  25823  abscxpbnd  25915  ang180lem2  25969  atanlogsublem  26074  atans2  26090  leibpi  26101  birthdaylem3  26112  cxplim  26130  cxp2limlem  26134  cxploglim2  26137  jensenlem2  26146  jensen  26147  amgmlem  26148  emcllem2  26155  emcllem4  26157  emcllem7  26160  zetacvg  26173  lgamgulmlem2  26188  lgamgulmlem5  26191  ftalem5  26235  basellem4  26242  basellem6  26244  basellem8  26246  basellem9  26247  chtwordi  26314  chpwordi  26315  ppiwordi  26320  ppiub  26361  vmalelog  26362  chtlepsi  26363  chtleppi  26367  chtublem  26368  chtub  26369  chpub  26377  logfaclbnd  26379  logfacrlim  26381  dchrptlem3  26423  bcmono  26434  bclbnd  26437  bposlem1  26441  bposlem6  26446  bposlem9  26449  lgsqrlem4  26506  2lgslem1c  26550  chebbnd1lem1  26626  chebbnd1lem3  26628  chebbnd1  26629  chtppilimlem1  26630  vmadivsum  26639  rplogsumlem2  26642  dchrisumlema  26645  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  dchrisum0flblem1  26665  dchrisum0re  26670  dchrisum0lem2a  26674  mulogsumlem  26688  mulog2sumlem1  26691  mulog2sumlem2  26692  2vmadivsumlem  26697  selberg2lem  26707  selberg3lem1  26714  selberg4lem1  26717  pntrlog2bndlem3  26736  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntpbnd1  26743  pntlemc  26752  pntlemr  26759  pntlemk  26763  pntlemo  26764  abvcxp  26772  ostth2lem1  26775  padicabv  26787  ostth2lem2  26791  ostth2lem3  26792  ostth2lem4  26793  ostth2  26794  legso  26969  trgcopy  27174  eucrct2eupth  28618  nvmtri  29042  imsmetlem  29061  vacn  29065  nmcvcn  29066  smcnlem  29068  blometi  29174  ipblnfi  29226  minvecolem2  29246  hhssnv  29635  nmcoplbi  30399  nmopcoi  30466  nmopcoadji  30472  idleop  30502  cdj1i  30804  isoun  31043  xlt2addrd  31090  mgcf1o  31290  omndmul  31349  ogrpsub  31351  gsumle  31359  cycpmconjslem2  31431  archirngz  31452  ofldchr  31522  lssdimle  31700  fedgmullem2  31720  pstmxmet  31856  nexple  31986  esumpmono  32056  esumcvg  32063  meascnbl  32196  omsmon  32274  omsmeas  32299  dstfrvinc  32452  hgt750lemd  32637  hgt750lema  32646  hgt750leme  32647  swrdwlk  33097  derangenlem  33142  subfaclefac  33147  subfaclim  33159  erdszelem10  33171  sinccvglem  33639  iprodefisum  33716  noextendlt  33881  noextendgt  33882  nosupbnd1  33926  nosupbnd2lem1  33927  noinfbnd1  33941  noinfbnd2lem1  33942  unbdqndv2lem2  34699  itg2gt0cn  35841  ibladdnclem  35842  iblabsnc  35850  iblmulc2nc  35851  itgabsnc  35855  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  mettrifi  35924  equivbnd2  35959  heiborlem6  35983  bfplem1  35989  bfp  35991  rrnmet  35996  rrndstprj1  35997  rrndstprj2  35998  dalawlem3  37894  dalawlem4  37895  dalawlem6  37897  dalawlem9  37900  dalawlem11  37902  dalawlem12  37903  dalawlem15  37906  cdleme3c  38251  cdleme7e  38268  cdleme26e  38380  cdleme26eALTN  38382  cdleme27a  38388  cdleme32c  38464  cdleme32e  38466  cdleme32le  38468  cdlemg9b  38654  cdlemg12b  38665  cdlemg12d  38667  trlcolem  38747  trlcone  38749  cdlemk7  38869  cdlemk7u  38891  cdlemk39  38937  cdlemk11ta  38950  cdlemk11tc  38966  mapdcnvatN  39687  factwoffsmonot  40170  frlmvscadiccat  40244  3cubeslem1  40513  irrapxlem5  40655  pell1qrge1  40699  pell1qrgaplem  40702  pell14qrgapw  40705  pellqrex  40708  pellfund14  40727  jm2.17a  40789  jm2.17c  40791  acongeq  40812  jm2.19  40822  jm2.27a  40834  jm2.27c  40836  jm3.1lem2  40847  areaquad  41054  rp-isfinite6  41132  hashnzfzclim  41947  binomcxplemnotnn0  41981  absimlere  43027  monoord2xrv  43031  ltmod  43186  dvbdfbdioolem2  43477  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweidlem3  43551  stoweidlem26  43574  wallispilem1  43613  wallispilem5  43617  stirlinglem1  43622  stirlinglem5  43626  stirlinglem8  43629  stirlinglem10  43631  stirlinglem12  43633  fourierdlem6  43661  fourierdlem7  43662  fourierdlem14  43669  fourierdlem19  43674  fourierdlem35  43690  fourierdlem39  43694  fourierdlem42  43697  fourierdlem50  43704  fourierdlem73  43727  fourierdlem76  43730  fourierdlem77  43731  fourierdlem81  43735  fourierdlem90  43744  fourierdlem92  43746  fourierdlem93  43747  fourierdlem111  43765  fouriersw  43779  etransclem38  43820  sge0split  43954  lighneallem4a  45071  rnghmsubcsetc  45546  rhmsubcsetc  45592  rhmsubcrngc  45598  rhmsubc  45659  rhmsubcALTV  45677  logbpw2m1  45924  dignn0flhalflem1  45972  dignn0flhalflem2  45973  1aryenef  46002  2aryenef  46013  2itscp  46138  amgmwlem  46517