Theorem 3brtr4d 5134

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5102

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103

This theorem is referenced by:  f1oiso2  7309  sucdom2  9144  ordtypelem6  9452  ttrcltr  9645  ttrclss  9649  ttrclselem2  9655  fin23lem26  10254  distrnq  10890  lediv12a  12052  recp1lt1  12057  ifle  13133  xleadd1a  13189  xlemul1a  13224  fldiv4p1lem1div2  13773  fldiv4lem1div2  13775  quoremz  13793  quoremnn0ALT  13795  intfracq  13797  modmulnn  13827  fzennn  13909  monoord2  13974  expgt1  14041  expmordi  14108  leexp2r  14115  leexp1a  14116  bernneq  14170  expmulnbnd  14176  digit1  14178  faclbnd  14231  faclbnd4lem3  14236  faclbnd4lem4  14237  faclbnd6  14240  facubnd  14241  hashdomi  14321  fzsdom2  14369  absrele  15250  absimle  15251  abstri  15273  abs2difabs  15277  limsupval2  15422  rlimrege0  15521  rlimrecl  15522  climsqz  15583  climsqz2  15584  rlimdiv  15588  rlimsqz  15592  rlimsqz2  15593  isercolllem1  15607  isercoll2  15611  fsumcvg2  15669  fsumrlim  15753  o1fsum  15755  cvgcmpce  15760  isumle  15786  climcndslem1  15791  climcndslem2  15792  harmonic  15801  expcnv  15806  explecnv  15807  geomulcvg  15818  efcllem  16019  ege2le3  16032  eflegeo  16065  rpnnen2lem4  16161  ruclem2  16176  ruclem8  16181  fsumdvds  16254  phibnd  16717  iserodd  16782  pcdvdstr  16823  pcprmpw2  16829  pockthg  16853  prmreclem4  16866  prmolefac  16993  2expltfac  17039  mod2ile  18429  odsubdvds  19477  pgpfi  19511  fislw  19531  efgredlemd  19650  efgredlem  19653  frgpcpbl  19665  rnghmsubcsetc  20518  rhmsubcsetc  20547  rhmsubcrngc  20553  rhmsubc  20574  abvres  20716  abvtrivd  20717  znrrg  21451  cstucnd  24147  psmetge0  24176  psmetres2  24178  xmetge0  24208  xmetres2  24225  imasf1oxmet  24239  comet  24377  stdbdxmet  24379  dscmet  24436  nrmmetd  24438  nmrtri  24488  tngngp  24518  nmolb2d  24582  nmoleub  24595  nmoco  24601  nmotri  24603  nmoid  24606  nmods  24608  cnmet  24635  xrsxmet  24674  metdstri  24716  metnrmlem3  24726  lebnumlem3  24838  ipcau2  25110  tcphcphlem1  25111  tcphcph  25113  trirn  25276  rrxmet  25284  rrxdstprj1  25285  minveclem2  25302  ovolunlem1a  25373  ovolscalem1  25390  volss  25410  voliunlem1  25427  volcn  25483  itg1climres  25591  mbfi1fseqlem5  25596  mbfi1fseqlem6  25597  itg2const2  25618  itg2seq  25619  itg2mulc  25624  itg2splitlem  25625  itg2monolem1  25627  itg2i1fseqle  25631  itg2i1fseq  25632  itg2i1fseq2  25633  itg2addlem  25635  itg2cnlem1  25638  itg2cnlem2  25639  iblss  25682  itgle  25687  ibladdlem  25697  iblabs  25706  iblabsr  25707  iblmulc2  25708  itgabs  25712  bddmulibl  25716  bddiblnc  25719  dvfsumabs  25905  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsum2  25917  deg1suble  25988  deg1mul3le  25998  plyeq0lem  26091  dgrcolem2  26156  geolim3  26223  aaliou3lem2  26227  aaliou3lem8  26229  ulmdvlem1  26285  radcnvlem1  26298  radcnvlem2  26299  dvradcnv  26306  pserulm  26307  pserdvlem2  26314  abelthlem2  26318  abelthlem5  26321  abelthlem7  26324  abelth2  26328  tangtx  26390  tanabsge  26391  tanord1  26422  argregt0  26495  argrege0  26496  argimgt0  26497  abslogle  26503  logcnlem4  26530  logtayllem  26544  abscxpbnd  26639  ang180lem2  26696  atanlogsublem  26801  atans2  26817  leibpi  26828  birthdaylem3  26839  cxplim  26858  cxp2limlem  26862  cxploglim2  26865  jensenlem2  26874  jensen  26875  amgmlem  26876  emcllem2  26883  emcllem4  26885  emcllem7  26888  zetacvg  26901  lgamgulmlem2  26916  lgamgulmlem5  26919  ftalem5  26963  basellem4  26970  basellem6  26972  basellem8  26974  basellem9  26975  chtwordi  27042  chpwordi  27043  ppiwordi  27048  ppiub  27091  vmalelog  27092  chtlepsi  27093  chtleppi  27097  chtublem  27098  chtub  27099  chpub  27107  logfaclbnd  27109  logfacrlim  27111  dchrptlem3  27153  bcmono  27164  bclbnd  27167  bposlem1  27171  bposlem6  27176  bposlem9  27179  lgsqrlem4  27236  2lgslem1c  27280  chebbnd1lem1  27356  chebbnd1lem3  27358  chebbnd1  27359  chtppilimlem1  27360  vmadivsum  27369  rplogsumlem2  27372  dchrisumlema  27375  dchrisumlem3  27378  dchrmusum2  27381  dchrvmasumlem3  27386  dchrvmasumiflem1  27388  dchrisum0flblem1  27395  dchrisum0re  27400  dchrisum0lem2a  27404  mulogsumlem  27418  mulog2sumlem1  27421  mulog2sumlem2  27422  2vmadivsumlem  27427  selberg2lem  27437  selberg3lem1  27444  selberg4lem1  27447  pntrlog2bndlem3  27466  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntpbnd1  27473  pntlemc  27482  pntlemr  27489  pntlemk  27493  pntlemo  27494  abvcxp  27502  ostth2lem1  27505  padicabv  27517  ostth2lem2  27521  ostth2lem3  27522  ostth2lem4  27523  ostth2  27524  noextendlt  27557  noextendgt  27558  nosupbnd1  27602  nosupbnd2lem1  27603  noinfbnd1  27617  noinfbnd2lem1  27618  lltropt  27760  addsproplem2  27853  addsproplem4  27855  addsproplem5  27856  addsproplem6  27857  mulsproplem5  27999  mulsproplem6  28000  mulsproplem7  28001  mulsproplem8  28002  slemuld  28017  mulsuniflem  28028  slemul1ad  28061  precsexlem9  28093  legso  28502  trgcopy  28707  eucrct2eupth  30147  nvmtri  30573  imsmetlem  30592  vacn  30596  nmcvcn  30597  smcnlem  30599  blometi  30705  ipblnfi  30757  minvecolem2  30777  hhssnv  31166  nmcoplbi  31930  nmopcoi  31997  nmopcoadji  32003  idleop  32033  cdj1i  32335  isoun  32598  xlt2addrd  32655  nexple  32742  mgcf1o  32902  pfxchn  32908  chnub  32911  chnccats1  32914  omndmul  33001  ogrpsub  33003  gsumle  33011  cycpmconjslem2  33085  archirngz  33116  elrgspnlem1  33166  ofldchr  33265  q1pvsca  33542  lssdimle  33576  fedgmullem2  33599  fldextrspundglemul  33647  fldext2chn  33691  2sqr3minply  33743  cos9thpiminply  33751  pstmxmet  33860  esumpmono  34042  esumcvg  34049  meascnbl  34182  omsmon  34262  omsmeas  34287  dstfrvinc  34441  hgt750lemd  34612  hgt750lema  34621  hgt750leme  34622  swrdwlk  35087  derangenlem  35131  subfaclefac  35136  subfaclim  35148  erdszelem10  35160  sinccvglem  35632  iprodefisum  35701  unbdqndv2lem2  36471  itg2gt0cn  37642  ibladdnclem  37643  iblabsnc  37651  iblmulc2nc  37652  itgabsnc  37656  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  mettrifi  37724  equivbnd2  37759  heiborlem6  37783  bfplem1  37789  bfp  37791  rrnmet  37796  rrndstprj1  37797  rrndstprj2  37798  dalawlem3  39840  dalawlem4  39841  dalawlem6  39843  dalawlem9  39846  dalawlem11  39848  dalawlem12  39849  dalawlem15  39852  cdleme3c  40197  cdleme7e  40214  cdleme26e  40326  cdleme26eALTN  40328  cdleme27a  40334  cdleme32c  40410  cdleme32e  40412  cdleme32le  40414  cdlemg9b  40600  cdlemg12b  40611  cdlemg12d  40613  trlcolem  40693  trlcone  40695  cdlemk7  40815  cdlemk7u  40837  cdlemk39  40883  cdlemk11ta  40896  cdlemk11tc  40912  mapdcnvatN  41633  explt1d  42284  frlmvscadiccat  42467  3cubeslem1  42645  irrapxlem5  42787  pell1qrge1  42831  pell1qrgaplem  42834  pell14qrgapw  42837  pellqrex  42840  pellfund14  42859  jm2.17a  42922  jm2.17c  42924  acongeq  42945  jm2.19  42955  jm2.27a  42967  jm2.27c  42969  jm3.1lem2  42980  areaquad  43178  rp-isfinite6  43480  hashnzfzclim  44284  binomcxplemnotnn0  44318  absimlere  45448  monoord2xrv  45452  ltmod  45609  liminflelimsuplem  45746  dvbdfbdioolem2  45900  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  stoweidlem3  45974  stoweidlem26  45997  wallispilem1  46036  wallispilem5  46040  stirlinglem1  46045  stirlinglem5  46049  stirlinglem8  46052  stirlinglem10  46054  stirlinglem12  46056  fourierdlem6  46084  fourierdlem7  46085  fourierdlem14  46092  fourierdlem19  46097  fourierdlem35  46113  fourierdlem39  46117  fourierdlem42  46120  fourierdlem50  46127  fourierdlem73  46150  fourierdlem76  46153  fourierdlem77  46154  fourierdlem81  46158  fourierdlem90  46167  fourierdlem92  46169  fourierdlem93  46170  fourierdlem111  46188  fouriersw  46202  etransclem38  46243  sge0split  46380  ovnsslelem  46531  lighneallem4a  47582  rhmsubcALTV  48246  logbpw2m1  48529  dignn0flhalflem1  48577  dignn0flhalflem2  48578  1aryenef  48607  2aryenef  48618  2itscp  48743  amgmwlem  49764