Theorem 3brtr4d 5121

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090

This theorem is referenced by:  f1oiso2  7281  sucdom2  9107  ordtypelem6  9404  ttrcltr  9601  ttrclss  9605  ttrclselem2  9611  fin23lem26  10208  distrnq  10844  lediv12a  12007  recp1lt1  12012  ifle  13088  xleadd1a  13144  xlemul1a  13179  fldiv4p1lem1div2  13731  fldiv4lem1div2  13733  quoremz  13751  quoremnn0ALT  13753  intfracq  13755  modmulnn  13785  fzennn  13867  monoord2  13932  expgt1  13999  expmordi  14066  leexp2r  14073  leexp1a  14074  bernneq  14128  expmulnbnd  14134  digit1  14136  faclbnd  14189  faclbnd4lem3  14194  faclbnd4lem4  14195  faclbnd6  14198  facubnd  14199  hashdomi  14279  fzsdom2  14327  absrele  15207  absimle  15208  abstri  15230  abs2difabs  15234  limsupval2  15379  rlimrege0  15478  rlimrecl  15479  climsqz  15540  climsqz2  15541  rlimdiv  15545  rlimsqz  15549  rlimsqz2  15550  isercolllem1  15564  isercoll2  15568  fsumcvg2  15626  fsumrlim  15710  o1fsum  15712  cvgcmpce  15717  isumle  15743  climcndslem1  15748  climcndslem2  15749  harmonic  15758  expcnv  15763  explecnv  15764  geomulcvg  15775  efcllem  15976  ege2le3  15989  eflegeo  16022  rpnnen2lem4  16118  ruclem2  16133  ruclem8  16138  fsumdvds  16211  phibnd  16674  iserodd  16739  pcdvdstr  16780  pcprmpw2  16786  pockthg  16810  prmreclem4  16823  prmolefac  16950  2expltfac  16996  mod2ile  18392  pfxchn  18508  chnub  18520  chnccats1  18523  chnccat  18524  chnrev  18525  ex-chn2  18536  odsubdvds  19476  pgpfi  19510  fislw  19530  efgredlemd  19649  efgredlem  19652  frgpcpbl  19664  omndmul  20040  ogrpsub  20042  gsumle  20050  rnghmsubcsetc  20541  rhmsubcsetc  20570  rhmsubcrngc  20576  rhmsubc  20597  abvres  20739  abvtrivd  20740  znrrg  21495  ofldchr  21506  cstucnd  24191  psmetge0  24220  psmetres2  24222  xmetge0  24252  xmetres2  24269  imasf1oxmet  24283  comet  24421  stdbdxmet  24423  dscmet  24480  nrmmetd  24482  nmrtri  24532  tngngp  24562  nmolb2d  24626  nmoleub  24639  nmoco  24645  nmotri  24647  nmoid  24650  nmods  24652  cnmet  24679  xrsxmet  24718  metdstri  24760  metnrmlem3  24770  lebnumlem3  24882  ipcau2  25154  tcphcphlem1  25155  tcphcph  25157  trirn  25320  rrxmet  25328  rrxdstprj1  25329  minveclem2  25346  ovolunlem1a  25417  ovolscalem1  25434  volss  25454  voliunlem1  25471  volcn  25527  itg1climres  25635  mbfi1fseqlem5  25640  mbfi1fseqlem6  25641  itg2const2  25662  itg2seq  25663  itg2mulc  25668  itg2splitlem  25669  itg2monolem1  25671  itg2i1fseqle  25675  itg2i1fseq  25676  itg2i1fseq2  25677  itg2addlem  25679  itg2cnlem1  25682  itg2cnlem2  25683  iblss  25726  itgle  25731  ibladdlem  25741  iblabs  25750  iblabsr  25751  iblmulc2  25752  itgabs  25756  bddmulibl  25760  bddiblnc  25763  dvfsumabs  25949  dvfsumlem2  25953  dvfsumlem2OLD  25954  dvfsum2  25961  deg1suble  26032  deg1mul3le  26042  plyeq0lem  26135  dgrcolem2  26200  geolim3  26267  aaliou3lem2  26271  aaliou3lem8  26273  ulmdvlem1  26329  radcnvlem1  26342  radcnvlem2  26343  dvradcnv  26350  pserulm  26351  pserdvlem2  26358  abelthlem2  26362  abelthlem5  26365  abelthlem7  26368  abelth2  26372  tangtx  26434  tanabsge  26435  tanord1  26466  argregt0  26539  argrege0  26540  argimgt0  26541  abslogle  26547  logcnlem4  26574  logtayllem  26588  abscxpbnd  26683  ang180lem2  26740  atanlogsublem  26845  atans2  26861  leibpi  26872  birthdaylem3  26883  cxplim  26902  cxp2limlem  26906  cxploglim2  26909  jensenlem2  26918  jensen  26919  amgmlem  26920  emcllem2  26927  emcllem4  26929  emcllem7  26932  zetacvg  26945  lgamgulmlem2  26960  lgamgulmlem5  26963  ftalem5  27007  basellem4  27014  basellem6  27016  basellem8  27018  basellem9  27019  chtwordi  27086  chpwordi  27087  ppiwordi  27092  ppiub  27135  vmalelog  27136  chtlepsi  27137  chtleppi  27141  chtublem  27142  chtub  27143  chpub  27151  logfaclbnd  27153  logfacrlim  27155  dchrptlem3  27197  bcmono  27208  bclbnd  27211  bposlem1  27215  bposlem6  27220  bposlem9  27223  lgsqrlem4  27280  2lgslem1c  27324  chebbnd1lem1  27400  chebbnd1lem3  27402  chebbnd1  27403  chtppilimlem1  27404  vmadivsum  27413  rplogsumlem2  27416  dchrisumlema  27419  dchrisumlem3  27422  dchrmusum2  27425  dchrvmasumlem3  27430  dchrvmasumiflem1  27432  dchrisum0flblem1  27439  dchrisum0re  27444  dchrisum0lem2a  27448  mulogsumlem  27462  mulog2sumlem1  27465  mulog2sumlem2  27466  2vmadivsumlem  27471  selberg2lem  27481  selberg3lem1  27488  selberg4lem1  27491  pntrlog2bndlem3  27510  pntrlog2bndlem5  27512  pntrlog2bndlem6  27514  pntpbnd1  27517  pntlemc  27526  pntlemr  27533  pntlemk  27537  pntlemo  27538  abvcxp  27546  ostth2lem1  27549  padicabv  27561  ostth2lem2  27565  ostth2lem3  27566  ostth2lem4  27567  ostth2  27568  noextendlt  27601  noextendgt  27602  nosupbnd1  27646  nosupbnd2lem1  27647  noinfbnd1  27661  noinfbnd2lem1  27662  lltropt  27810  addsproplem2  27906  addsproplem4  27908  addsproplem5  27909  addsproplem6  27910  mulsproplem5  28052  mulsproplem6  28053  mulsproplem7  28054  mulsproplem8  28055  slemuld  28070  mulsuniflem  28081  slemul1ad  28114  precsexlem9  28146  legso  28570  trgcopy  28775  eucrct2eupth  30215  nvmtri  30641  imsmetlem  30660  vacn  30664  nmcvcn  30665  smcnlem  30667  blometi  30773  ipblnfi  30825  minvecolem2  30845  hhssnv  31234  nmcoplbi  31998  nmopcoi  32065  nmopcoadji  32071  idleop  32101  cdj1i  32403  isoun  32673  xlt2addrd  32732  nexple  32817  mgcf1o  32974  cycpmconjslem2  33114  archirngz  33148  elrgspnlem1  33199  q1pvsca  33554  lssdimle  33610  fedgmullem2  33633  fldextrspundglemul  33682  extdgfialglem1  33695  fldext2chn  33731  2sqr3minply  33783  cos9thpiminply  33791  pstmxmet  33900  esumpmono  34082  esumcvg  34089  meascnbl  34222  omsmon  34301  omsmeas  34326  dstfrvinc  34480  hgt750lemd  34651  hgt750lema  34660  hgt750leme  34661  swrdwlk  35139  derangenlem  35183  subfaclefac  35188  subfaclim  35200  erdszelem10  35212  sinccvglem  35684  iprodefisum  35753  unbdqndv2lem2  36523  itg2gt0cn  37694  ibladdnclem  37695  iblabsnc  37703  iblmulc2nc  37704  itgabsnc  37708  ftc1anclem7  37718  ftc1anclem8  37719  ftc1anc  37720  mettrifi  37776  equivbnd2  37811  heiborlem6  37835  bfplem1  37841  bfp  37843  rrnmet  37848  rrndstprj1  37849  rrndstprj2  37850  dalawlem3  39891  dalawlem4  39892  dalawlem6  39894  dalawlem9  39897  dalawlem11  39899  dalawlem12  39900  dalawlem15  39903  cdleme3c  40248  cdleme7e  40265  cdleme26e  40377  cdleme26eALTN  40379  cdleme27a  40385  cdleme32c  40461  cdleme32e  40463  cdleme32le  40465  cdlemg9b  40651  cdlemg12b  40662  cdlemg12d  40664  trlcolem  40744  trlcone  40746  cdlemk7  40866  cdlemk7u  40888  cdlemk39  40934  cdlemk11ta  40947  cdlemk11tc  40963  mapdcnvatN  41684  explt1d  42335  frlmvscadiccat  42518  3cubeslem1  42696  irrapxlem5  42838  pell1qrge1  42882  pell1qrgaplem  42885  pell14qrgapw  42888  pellqrex  42891  pellfund14  42910  jm2.17a  42972  jm2.17c  42974  acongeq  42995  jm2.19  43005  jm2.27a  43017  jm2.27c  43019  jm3.1lem2  43030  areaquad  43228  rp-isfinite6  43530  hashnzfzclim  44334  binomcxplemnotnn0  44368  absimlere  45496  monoord2xrv  45500  ltmod  45655  liminflelimsuplem  45792  dvbdfbdioolem2  45946  ioodvbdlimc1lem2  45949  ioodvbdlimc2lem  45951  stoweidlem3  46020  stoweidlem26  46043  wallispilem1  46082  wallispilem5  46086  stirlinglem1  46091  stirlinglem5  46095  stirlinglem8  46098  stirlinglem10  46100  stirlinglem12  46102  fourierdlem6  46130  fourierdlem7  46131  fourierdlem14  46138  fourierdlem19  46143  fourierdlem35  46159  fourierdlem39  46163  fourierdlem42  46166  fourierdlem50  46173  fourierdlem73  46196  fourierdlem76  46199  fourierdlem77  46200  fourierdlem81  46204  fourierdlem90  46213  fourierdlem92  46215  fourierdlem93  46216  fourierdlem111  46234  fouriersw  46248  etransclem38  46289  sge0split  46426  ovnsslelem  46577  lighneallem4a  47618  rhmsubcALTV  48295  logbpw2m1  48578  dignn0flhalflem1  48626  dignn0flhalflem2  48627  1aryenef  48656  2aryenef  48667  2itscp  48792  amgmwlem  49813