Theorem 3brtr4d 5179

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

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

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148

This theorem is referenced by:  f1oiso2  7351  sucdom2OLD  9084  sucdom2  9208  ordtypelem6  9520  ttrcltr  9713  ttrclss  9717  ttrclselem2  9723  fin23lem26  10322  distrnq  10958  lediv12a  12111  recp1lt1  12116  ifle  13180  xleadd1a  13236  xlemul1a  13271  fldiv4p1lem1div2  13804  fldiv4lem1div2  13806  quoremz  13824  quoremnn0ALT  13826  intfracq  13828  modmulnn  13858  fzennn  13937  monoord2  14003  expgt1  14070  expmordi  14136  leexp2r  14143  leexp1a  14144  bernneq  14196  expmulnbnd  14202  digit1  14204  faclbnd  14254  faclbnd4lem3  14259  faclbnd4lem4  14260  faclbnd6  14263  facubnd  14264  hashdomi  14344  fzsdom2  14392  absrele  15259  absimle  15260  abstri  15281  abs2difabs  15285  limsupval2  15428  rlimrege0  15527  rlimrecl  15528  climsqz  15589  climsqz2  15590  rlimdiv  15596  rlimsqz  15600  rlimsqz2  15601  isercolllem1  15615  isercoll2  15619  fsumcvg2  15677  fsumrlim  15761  o1fsum  15763  cvgcmpce  15768  isumle  15794  climcndslem1  15799  climcndslem2  15800  harmonic  15809  expcnv  15814  explecnv  15815  geomulcvg  15826  efcllem  16025  ege2le3  16037  eflegeo  16068  rpnnen2lem4  16164  ruclem2  16179  ruclem8  16184  fsumdvds  16255  phibnd  16708  iserodd  16772  pcdvdstr  16813  pcprmpw2  16819  pockthg  16843  prmreclem4  16856  prmolefac  16983  2expltfac  17030  mod2ile  18451  odsubdvds  19480  pgpfi  19514  fislw  19534  efgredlemd  19653  efgredlem  19656  frgpcpbl  19668  abvres  20590  abvtrivd  20591  znrrg  21340  cstucnd  24009  psmetge0  24038  psmetres2  24040  xmetge0  24070  xmetres2  24087  imasf1oxmet  24101  comet  24242  stdbdxmet  24244  dscmet  24301  nrmmetd  24303  nmrtri  24353  tngngp  24391  nmolb2d  24455  nmoleub  24468  nmoco  24474  nmotri  24476  nmoid  24479  nmods  24481  cnmet  24508  xrsxmet  24545  metdstri  24587  metnrmlem3  24597  lebnumlem3  24709  ipcau2  24982  tcphcphlem1  24983  tcphcph  24985  trirn  25148  rrxmet  25156  rrxdstprj1  25157  minveclem2  25174  ovolunlem1a  25245  ovolscalem1  25262  volss  25282  voliunlem1  25299  volcn  25355  itg1climres  25464  mbfi1fseqlem5  25469  mbfi1fseqlem6  25470  itg2const2  25491  itg2seq  25492  itg2mulc  25497  itg2splitlem  25498  itg2monolem1  25500  itg2i1fseqle  25504  itg2i1fseq  25505  itg2i1fseq2  25506  itg2addlem  25508  itg2cnlem1  25511  itg2cnlem2  25512  iblss  25554  itgle  25559  ibladdlem  25569  iblabs  25578  iblabsr  25579  iblmulc2  25580  itgabs  25584  bddmulibl  25588  bddiblnc  25591  dvfsumabs  25775  dvfsumlem2  25779  dvfsum2  25786  deg1suble  25860  deg1mul3le  25869  plyeq0lem  25959  dgrcolem2  26024  geolim3  26088  aaliou3lem2  26092  aaliou3lem8  26094  ulmdvlem1  26148  radcnvlem1  26161  radcnvlem2  26162  dvradcnv  26169  pserulm  26170  pserdvlem2  26176  abelthlem2  26180  abelthlem5  26183  abelthlem7  26186  abelth2  26190  tangtx  26251  tanabsge  26252  tanord1  26282  argregt0  26354  argrege0  26355  argimgt0  26356  abslogle  26362  logcnlem4  26389  logtayllem  26403  abscxpbnd  26497  ang180lem2  26551  atanlogsublem  26656  atans2  26672  leibpi  26683  birthdaylem3  26694  cxplim  26712  cxp2limlem  26716  cxploglim2  26719  jensenlem2  26728  jensen  26729  amgmlem  26730  emcllem2  26737  emcllem4  26739  emcllem7  26742  zetacvg  26755  lgamgulmlem2  26770  lgamgulmlem5  26773  ftalem5  26817  basellem4  26824  basellem6  26826  basellem8  26828  basellem9  26829  chtwordi  26896  chpwordi  26897  ppiwordi  26902  ppiub  26943  vmalelog  26944  chtlepsi  26945  chtleppi  26949  chtublem  26950  chtub  26951  chpub  26959  logfaclbnd  26961  logfacrlim  26963  dchrptlem3  27005  bcmono  27016  bclbnd  27019  bposlem1  27023  bposlem6  27028  bposlem9  27031  lgsqrlem4  27088  2lgslem1c  27132  chebbnd1lem1  27208  chebbnd1lem3  27210  chebbnd1  27211  chtppilimlem1  27212  vmadivsum  27221  rplogsumlem2  27224  dchrisumlema  27227  dchrisumlem3  27230  dchrmusum2  27233  dchrvmasumlem3  27238  dchrvmasumiflem1  27240  dchrisum0flblem1  27247  dchrisum0re  27252  dchrisum0lem2a  27256  mulogsumlem  27270  mulog2sumlem1  27273  mulog2sumlem2  27274  2vmadivsumlem  27279  selberg2lem  27289  selberg3lem1  27296  selberg4lem1  27299  pntrlog2bndlem3  27318  pntrlog2bndlem5  27320  pntrlog2bndlem6  27322  pntpbnd1  27325  pntlemc  27334  pntlemr  27341  pntlemk  27345  pntlemo  27346  abvcxp  27354  ostth2lem1  27357  padicabv  27369  ostth2lem2  27373  ostth2lem3  27374  ostth2lem4  27375  ostth2  27376  noextendlt  27408  noextendgt  27409  nosupbnd1  27453  nosupbnd2lem1  27454  noinfbnd1  27468  noinfbnd2lem1  27469  lltropt  27604  addsproplem2  27692  addsproplem4  27694  addsproplem5  27695  addsproplem6  27696  mulsproplem5  27815  mulsproplem6  27816  mulsproplem7  27817  mulsproplem8  27818  slemuld  27833  mulsuniflem  27843  precsexlem9  27900  legso  28117  trgcopy  28322  eucrct2eupth  29765  nvmtri  30191  imsmetlem  30210  vacn  30214  nmcvcn  30215  smcnlem  30217  blometi  30323  ipblnfi  30375  minvecolem2  30395  hhssnv  30784  nmcoplbi  31548  nmopcoi  31615  nmopcoadji  31621  idleop  31651  cdj1i  31953  isoun  32190  xlt2addrd  32238  mgcf1o  32440  omndmul  32502  ogrpsub  32504  gsumle  32512  cycpmconjslem2  32584  archirngz  32605  ofldchr  32702  q1pvsca  32949  lssdimle  32980  fedgmullem2  33003  pstmxmet  33175  nexple  33305  esumpmono  33375  esumcvg  33382  meascnbl  33515  omsmon  33595  omsmeas  33620  dstfrvinc  33773  hgt750lemd  33958  hgt750lema  33967  hgt750leme  33968  swrdwlk  34415  derangenlem  34460  subfaclefac  34465  subfaclim  34477  erdszelem10  34489  sinccvglem  34955  iprodefisum  35015  gg-dvfsumlem2  35469  unbdqndv2lem2  35689  itg2gt0cn  36846  ibladdnclem  36847  iblabsnc  36855  iblmulc2nc  36856  itgabsnc  36860  ftc1anclem7  36870  ftc1anclem8  36871  ftc1anc  36872  mettrifi  36928  equivbnd2  36963  heiborlem6  36987  bfplem1  36993  bfp  36995  rrnmet  37000  rrndstprj1  37001  rrndstprj2  37002  dalawlem3  39047  dalawlem4  39048  dalawlem6  39050  dalawlem9  39053  dalawlem11  39055  dalawlem12  39056  dalawlem15  39059  cdleme3c  39404  cdleme7e  39421  cdleme26e  39533  cdleme26eALTN  39535  cdleme27a  39541  cdleme32c  39617  cdleme32e  39619  cdleme32le  39621  cdlemg9b  39807  cdlemg12b  39818  cdlemg12d  39820  trlcolem  39900  trlcone  39902  cdlemk7  40022  cdlemk7u  40044  cdlemk39  40090  cdlemk11ta  40103  cdlemk11tc  40119  mapdcnvatN  40840  factwoffsmonot  41329  frlmvscadiccat  41386  3cubeslem1  41724  irrapxlem5  41866  pell1qrge1  41910  pell1qrgaplem  41913  pell14qrgapw  41916  pellqrex  41919  pellfund14  41938  jm2.17a  42001  jm2.17c  42003  acongeq  42024  jm2.19  42034  jm2.27a  42046  jm2.27c  42048  jm3.1lem2  42059  areaquad  42267  rp-isfinite6  42571  hashnzfzclim  43383  binomcxplemnotnn0  43417  absimlere  44488  monoord2xrv  44492  ltmod  44652  dvbdfbdioolem2  44943  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  stoweidlem3  45017  stoweidlem26  45040  wallispilem1  45079  wallispilem5  45083  stirlinglem1  45088  stirlinglem5  45092  stirlinglem8  45095  stirlinglem10  45097  stirlinglem12  45099  fourierdlem6  45127  fourierdlem7  45128  fourierdlem14  45135  fourierdlem19  45140  fourierdlem35  45156  fourierdlem39  45160  fourierdlem42  45163  fourierdlem50  45170  fourierdlem73  45193  fourierdlem76  45196  fourierdlem77  45197  fourierdlem81  45201  fourierdlem90  45210  fourierdlem92  45212  fourierdlem93  45213  fourierdlem111  45231  fouriersw  45245  etransclem38  45286  sge0split  45423  ovnsslelem  45574  lighneallem4a  46574  rnghmsubcsetc  46963  rhmsubcsetc  47009  rhmsubcrngc  47015  rhmsubc  47076  rhmsubcALTV  47094  logbpw2m1  47340  dignn0flhalflem1  47388  dignn0flhalflem2  47389  1aryenef  47418  2aryenef  47429  2itscp  47554  amgmwlem  47936