Theorem 3brtr4d 5143

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

Syntax hints:   → wi 4   = wceq 1570   class class class wbr 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110

This theorem is referenced by:  f1oiso2  7350  sucdom2  9183  ordtypelem6  9481  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  fin23lem26  10304  distrnq  10941  lediv12a  12103  recp1lt1  12108  ifle  13218  xleadd1a  13274  xlemul1a  13309  fldiv4p1lem1div2  13864  fldiv4lem1div2  13866  quoremz  13884  quoremnn0ALT  13886  intfracq  13888  modmulnn  13918  fzennn  14000  monoord2  14065  expgt1  14132  expmordi  14199  leexp2r  14206  leexp1a  14207  bernneq  14261  expmulnbnd  14267  digit1  14269  faclbnd  14322  faclbnd4lem3  14327  faclbnd4lem4  14328  faclbnd6  14331  facubnd  14332  hashdomi  14412  fzsdom2  14461  absrele  15355  absimle  15356  abstri  15378  abs2difabs  15382  limsupval2  15527  rlimrege0  15626  rlimrecl  15627  climsqz  15688  climsqz2  15689  rlimdiv  15693  rlimsqz  15697  rlimsqz2  15698  isercolllem1  15712  isercoll2  15716  fsumcvg2  15774  fsumrlim  15859  o1fsum  15861  cvgcmpce  15866  isumle  15894  climcndslem1  15899  climcndslem2  15900  harmonic  15909  expcnv  15914  explecnv  15915  geomulcvg  15926  efcllem  16126  ege2le3  16139  eflegeo  16172  rpnnen2lem4  16268  ruclem2  16283  ruclem8  16288  fsumdvds  16361  phibnd  16825  iserodd  16890  pcdvdstr  16931  pcprmpw2  16937  pockthg  16961  prmreclem4  16974  prmolefac  17101  2expltfac  17147  mod2ile  18545  pfxchn  18661  chnub  18673  chnccats1  18676  chnccat  18677  chnrev  18678  ex-chn2  18689  odsubdvds  19636  pgpfi  19670  fislw  19690  efgredlemd  19809  efgredlem  19812  frgpcpbl  19824  omndmul  20200  ogrpsub  20202  gsumle  20210  rnghmsubcsetc  20732  rhmsubcsetc  20761  rhmsubcrngc  20767  rhmsubc  20788  abvres  20934  abvtrivd  20935  znrrg  21715  ofldchr  21726  cstucnd  24440  psmetge0  24469  psmetres2  24471  xmetge0  24501  xmetres2  24518  imasf1oxmet  24532  comet  24670  stdbdxmet  24672  dscmet  24729  nrmmetd  24731  nmrtri  24781  tngngp  24811  nmolb2d  24875  nmoleub  24888  nmoco  24894  nmotri  24896  nmoid  24899  nmods  24901  cnmet  24928  xrsxmet  24967  metdstri  25009  metnrmlem3  25019  lebnumlem3  25122  ipcau2  25393  tcphcphlem1  25394  tcphcph  25396  trirn  25559  rrxmet  25567  rrxdstprj1  25568  minveclem2  25585  ovolunlem1a  25655  ovolscalem1  25672  volss  25692  voliunlem1  25709  volcn  25765  itg1climres  25873  mbfi1fseqlem5  25878  mbfi1fseqlem6  25879  itg2const2  25900  itg2seq  25901  itg2mulc  25906  itg2splitlem  25907  itg2monolem1  25909  itg2i1fseqle  25913  itg2i1fseq  25914  itg2i1fseq2  25915  itg2addlem  25917  itg2cnlem1  25920  itg2cnlem2  25921  iblss  25964  itgle  25969  ibladdlem  25979  iblabs  25988  iblabsr  25989  iblmulc2  25990  itgabs  25994  bddmulibl  25998  bddiblnc  26001  dvfsumabs  26182  dvfsumlem2  26186  dvfsum2  26193  deg1suble  26264  deg1mul3le  26274  plyeq0lem  26367  dgrcolem2  26431  geolim3  26502  aaliou3lem2  26506  aaliou3lem8  26508  ulmdvlem1  26563  radcnvlem1  26576  radcnvlem2  26577  dvradcnv  26584  pserulm  26585  pserdvlem2  26591  abelthlem2  26595  abelthlem5  26598  abelthlem7  26601  abelth2  26605  tangtx  26670  tanabsge  26671  tanord1  26702  argregt0  26775  argrege0  26776  argimgt0  26777  abslogle  26783  logcnlem4  26810  logtayllem  26824  abscxpbnd  26918  ang180lem2  26975  atanlogsublem  27080  atans2  27096  leibpi  27107  birthdaylem3  27118  cxplim  27136  cxp2limlem  27140  cxploglim2  27143  jensenlem2  27152  jensen  27153  amgmlem  27154  emcllem2  27161  emcllem4  27163  emcllem7  27166  zetacvg  27179  lgamgulmlem2  27194  lgamgulmlem5  27197  ftalem5  27241  basellem4  27248  basellem6  27250  basellem8  27252  basellem9  27253  chtwordi  27320  chpwordi  27321  ppiwordi  27326  ppiub  27368  vmalelog  27369  chtlepsi  27370  chtleppi  27374  chtublem  27375  chtub  27376  chpub  27384  logfaclbnd  27386  logfacrlim  27388  dchrptlem3  27430  bcmono  27441  bclbnd  27444  bposlem1  27448  bposlem6  27453  bposlem9  27456  lgsqrlem4  27513  2lgslem1c  27557  chebbnd1lem1  27633  chebbnd1lem3  27635  chebbnd1  27636  chtppilimlem1  27637  vmadivsum  27646  rplogsumlem2  27649  dchrisumlema  27652  dchrisumlem3  27655  dchrmusum2  27658  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  dchrisum0flblem1  27672  dchrisum0re  27677  dchrisum0lem2a  27681  mulogsumlem  27695  mulog2sumlem1  27698  mulog2sumlem2  27699  2vmadivsumlem  27704  selberg2lem  27714  selberg3lem1  27721  selberg4lem1  27724  pntrlog2bndlem3  27743  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntpbnd1  27750  pntlemc  27759  pntlemr  27766  pntlemk  27770  pntlemo  27771  abvcxp  27779  ostth2lem1  27782  padicabv  27794  ostth2lem2  27798  ostth2lem3  27799  ostth2lem4  27800  ostth2  27801  noextendlt  27833  noextendgt  27834  nosupbnd1  27878  nosupbnd2lem1  27879  noinfbnd1  27893  noinfbnd2lem1  27894  lltr  28055  addsproplem2  28163  addsproplem4  28165  addsproplem5  28166  addsproplem6  28167  mulsproplem5  28313  mulsproplem6  28314  mulsproplem7  28315  mulsproplem8  28316  lemulsd  28331  mulsuniflem  28342  lemuls1ad  28375  precsexlem9  28408  bdaypw2n0bndlem  28656  legso  28868  trgcopy  29115  eucrct2eupth  30596  nvmtri  31023  imsmetlem  31042  vacn  31046  nmcvcn  31047  smcnlem  31049  blometi  31155  ipblnfi  31207  minvecolem2  31227  hhssnv  31616  nmcoplbi  32380  nmopcoi  32447  nmopcoadji  32453  idleop  32483  cdj1i  32785  isoun  33047  xlt2addrd  33104  nexple  33177  mgcf1o  33323  cycpmconjslem2  33475  archirngz  33509  elrgspnlem1  33562  q1pvsca  33894  lssdimle  33998  fedgmullem2  34020  fldextrspundglemul  34069  extdgfialglem1  34082  fldext2chn  34118  2sqr3minply  34170  cos9thpiminply  34178  pstmxmet  34287  esumpmono  34469  esumcvg  34476  meascnbl  34609  omsmon  34688  omsmeas  34713  dstfrvinc  34867  hgt750lemd  35035  hgt750lema  35044  hgt750leme  35045  swrdwlk  35619  derangenlem  35663  subfaclefac  35668  subfaclim  35680  erdszelem10  35692  sinccvglem  36164  iprodefisum  36233  unbdqndv2lem2  37099  itg2gt0cn  38326  ibladdnclem  38327  iblabsnc  38335  iblmulc2nc  38336  itgabsnc  38340  ftc1anclem7  38350  ftc1anclem8  38351  ftc1anc  38352  mettrifi  38408  equivbnd2  38443  heiborlem6  38467  bfplem1  38473  bfp  38475  rrnmet  38480  rrndstprj1  38481  rrndstprj2  38482  dalawlem3  40647  dalawlem4  40648  dalawlem6  40650  dalawlem9  40653  dalawlem11  40655  dalawlem12  40656  dalawlem15  40659  cdleme3c  41004  cdleme7e  41021  cdleme26e  41133  cdleme26eALTN  41135  cdleme27a  41141  cdleme32c  41217  cdleme32e  41219  cdleme32le  41221  cdlemg9b  41407  cdlemg12b  41418  cdlemg12d  41420  trlcolem  41500  trlcone  41502  cdlemk7  41622  cdlemk7u  41644  cdlemk39  41690  cdlemk11ta  41703  cdlemk11tc  41719  mapdcnvatN  42440  explt1d  43084  frlmvscadiccat  43280  3cubeslem1  43415  irrapxlem5  43553  pell1qrge1  43597  pell1qrgaplem  43600  pell14qrgapw  43603  pellqrex  43606  pellfund14  43625  jm2.17a  43687  jm2.17c  43689  acongeq  43710  jm2.19  43720  jm2.27a  43732  jm2.27c  43734  jm3.1lem2  43745  areaquad  43943  rp-isfinite6  44244  hashnzfzclim  45032  binomcxplemnotnn0  45066  absimlere  46193  monoord2xrv  46197  ltmod  46352  liminflelimsuplem  46489  dvbdfbdioolem2  46643  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  stoweidlem3  46717  stoweidlem26  46740  wallispilem1  46779  wallispilem5  46783  stirlinglem1  46788  stirlinglem5  46792  stirlinglem8  46795  stirlinglem10  46797  stirlinglem12  46799  fourierdlem6  46827  fourierdlem7  46828  fourierdlem14  46835  fourierdlem19  46840  fourierdlem35  46856  fourierdlem39  46860  fourierdlem42  46863  fourierdlem50  46870  fourierdlem73  46893  fourierdlem76  46896  fourierdlem77  46897  fourierdlem81  46901  fourierdlem90  46910  fourierdlem92  46912  fourierdlem93  46913  fourierdlem111  46931  fouriersw  46945  etransclem38  46986  sge0split  47123  ovnsslelem  47274  chnsubseq  47596  chnsuslle  47597  chnerlem1  47598  lighneallem4a  48360  rhmsubcALTV  49050  logbpw2m1  49347  dignn0flhalflem1  49395  dignn0flhalflem2  49396  1aryenef  49425  2aryenef  49436  2itscp  49561  amgmwlem  50622