Theorem 3brtr4d 5144

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

Syntax hints:   → wi 4   = wceq 1567   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  f1oiso2  7348  sucdom2  9183  ordtypelem6  9481  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  fin23lem26  10305  distrnq  10942  lediv12a  12104  recp1lt1  12109  ifle  13219  xleadd1a  13275  xlemul1a  13310  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  16127  ege2le3  16140  eflegeo  16173  rpnnen2lem4  16269  ruclem2  16284  ruclem8  16289  fsumdvds  16362  phibnd  16826  iserodd  16891  pcdvdstr  16932  pcprmpw2  16938  pockthg  16962  prmreclem4  16975  prmolefac  17102  2expltfac  17148  mod2ile  18546  pfxchn  18662  chnub  18674  chnccats1  18677  chnccat  18678  chnrev  18679  ex-chn2  18690  odsubdvds  19637  pgpfi  19671  fislw  19691  efgredlemd  19810  efgredlem  19813  frgpcpbl  19825  omndmul  20201  ogrpsub  20203  gsumle  20211  rnghmsubcsetc  20714  rhmsubcsetc  20743  rhmsubcrngc  20749  rhmsubc  20770  abvres  20908  abvtrivd  20909  znrrg  21680  ofldchr  21691  cstucnd  24405  psmetge0  24434  psmetres2  24436  xmetge0  24466  xmetres2  24483  imasf1oxmet  24497  comet  24635  stdbdxmet  24637  dscmet  24694  nrmmetd  24696  nmrtri  24746  tngngp  24776  nmolb2d  24840  nmoleub  24853  nmoco  24859  nmotri  24861  nmoid  24864  nmods  24866  cnmet  24893  xrsxmet  24932  metdstri  24974  metnrmlem3  24984  lebnumlem3  25087  ipcau2  25358  tcphcphlem1  25359  tcphcph  25361  trirn  25524  rrxmet  25532  rrxdstprj1  25533  minveclem2  25550  ovolunlem1a  25620  ovolscalem1  25637  volss  25657  voliunlem1  25674  volcn  25730  itg1climres  25838  mbfi1fseqlem5  25843  mbfi1fseqlem6  25844  itg2const2  25865  itg2seq  25866  itg2mulc  25871  itg2splitlem  25872  itg2monolem1  25874  itg2i1fseqle  25878  itg2i1fseq  25879  itg2i1fseq2  25880  itg2addlem  25882  itg2cnlem1  25885  itg2cnlem2  25886  iblss  25929  itgle  25934  ibladdlem  25944  iblabs  25953  iblabsr  25954  iblmulc2  25955  itgabs  25959  bddmulibl  25963  bddiblnc  25966  dvfsumabs  26147  dvfsumlem2  26151  dvfsum2  26158  deg1suble  26229  deg1mul3le  26239  plyeq0lem  26332  dgrcolem2  26396  geolim3  26465  aaliou3lem2  26469  aaliou3lem8  26471  ulmdvlem1  26525  radcnvlem1  26538  radcnvlem2  26539  dvradcnv  26546  pserulm  26547  pserdvlem2  26553  abelthlem2  26557  abelthlem5  26560  abelthlem7  26563  abelth2  26567  tangtx  26632  tanabsge  26633  tanord1  26664  argregt0  26737  argrege0  26738  argimgt0  26739  abslogle  26745  logcnlem4  26772  logtayllem  26786  abscxpbnd  26880  ang180lem2  26937  atanlogsublem  27042  atans2  27058  leibpi  27069  birthdaylem3  27080  cxplim  27098  cxp2limlem  27102  cxploglim2  27105  jensenlem2  27114  jensen  27115  amgmlem  27116  emcllem2  27123  emcllem4  27125  emcllem7  27128  zetacvg  27141  lgamgulmlem2  27156  lgamgulmlem5  27159  ftalem5  27203  basellem4  27210  basellem6  27212  basellem8  27214  basellem9  27215  chtwordi  27282  chpwordi  27283  ppiwordi  27288  ppiub  27330  vmalelog  27331  chtlepsi  27332  chtleppi  27336  chtublem  27337  chtub  27338  chpub  27346  logfaclbnd  27348  logfacrlim  27350  dchrptlem3  27392  bcmono  27403  bclbnd  27406  bposlem1  27410  bposlem6  27415  bposlem9  27418  lgsqrlem4  27475  2lgslem1c  27519  chebbnd1lem1  27595  chebbnd1lem3  27597  chebbnd1  27598  chtppilimlem1  27599  vmadivsum  27608  rplogsumlem2  27611  dchrisumlema  27614  dchrisumlem3  27617  dchrmusum2  27620  dchrvmasumlem3  27625  dchrvmasumiflem1  27627  dchrisum0flblem1  27634  dchrisum0re  27639  dchrisum0lem2a  27643  mulogsumlem  27657  mulog2sumlem1  27660  mulog2sumlem2  27661  2vmadivsumlem  27666  selberg2lem  27676  selberg3lem1  27683  selberg4lem1  27686  pntrlog2bndlem3  27705  pntrlog2bndlem5  27707  pntrlog2bndlem6  27709  pntpbnd1  27712  pntlemc  27721  pntlemr  27728  pntlemk  27732  pntlemo  27733  abvcxp  27741  ostth2lem1  27744  padicabv  27756  ostth2lem2  27760  ostth2lem3  27761  ostth2lem4  27762  ostth2  27763  noextendlt  27795  noextendgt  27796  nosupbnd1  27840  nosupbnd2lem1  27841  noinfbnd1  27855  noinfbnd2lem1  27856  lltr  28017  addsproplem2  28125  addsproplem4  28127  addsproplem5  28128  addsproplem6  28129  mulsproplem5  28275  mulsproplem6  28276  mulsproplem7  28277  mulsproplem8  28278  lemulsd  28293  mulsuniflem  28304  lemuls1ad  28337  precsexlem9  28370  bdaypw2n0bndlem  28618  legso  28830  trgcopy  29068  eucrct2eupth  30533  nvmtri  30960  imsmetlem  30979  vacn  30983  nmcvcn  30984  smcnlem  30986  blometi  31092  ipblnfi  31144  minvecolem2  31164  hhssnv  31553  nmcoplbi  32317  nmopcoi  32384  nmopcoadji  32390  idleop  32420  cdj1i  32722  isoun  32984  xlt2addrd  33041  nexple  33114  mgcf1o  33260  cycpmconjslem2  33412  archirngz  33446  elrgspnlem1  33499  q1pvsca  33835  lssdimle  33939  fedgmullem2  33961  fldextrspundglemul  34010  extdgfialglem1  34023  fldext2chn  34059  2sqr3minply  34111  cos9thpiminply  34119  pstmxmet  34228  esumpmono  34410  esumcvg  34417  meascnbl  34550  omsmon  34629  omsmeas  34654  dstfrvinc  34808  hgt750lemd  34976  hgt750lema  34985  hgt750leme  34986  swrdwlk  35514  derangenlem  35558  subfaclefac  35563  subfaclim  35575  erdszelem10  35587  sinccvglem  36059  iprodefisum  36128  unbdqndv2lem2  36984  itg2gt0cn  38209  ibladdnclem  38210  iblabsnc  38218  iblmulc2nc  38219  itgabsnc  38223  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  mettrifi  38291  equivbnd2  38326  heiborlem6  38350  bfplem1  38356  bfp  38358  rrnmet  38363  rrndstprj1  38364  rrndstprj2  38365  dalawlem3  40532  dalawlem4  40533  dalawlem6  40535  dalawlem9  40538  dalawlem11  40540  dalawlem12  40541  dalawlem15  40544  cdleme3c  40889  cdleme7e  40906  cdleme26e  41018  cdleme26eALTN  41020  cdleme27a  41026  cdleme32c  41102  cdleme32e  41104  cdleme32le  41106  cdlemg9b  41292  cdlemg12b  41303  cdlemg12d  41305  trlcolem  41385  trlcone  41387  cdlemk7  41507  cdlemk7u  41529  cdlemk39  41575  cdlemk11ta  41588  cdlemk11tc  41604  mapdcnvatN  42325  explt1d  42969  frlmvscadiccat  43165  3cubeslem1  43302  irrapxlem5  43440  pell1qrge1  43484  pell1qrgaplem  43487  pell14qrgapw  43490  pellqrex  43493  pellfund14  43512  jm2.17a  43574  jm2.17c  43576  acongeq  43597  jm2.19  43607  jm2.27a  43619  jm2.27c  43621  jm3.1lem2  43632  areaquad  43830  rp-isfinite6  44131  hashnzfzclim  44919  binomcxplemnotnn0  44953  absimlere  46080  monoord2xrv  46084  ltmod  46239  liminflelimsuplem  46376  dvbdfbdioolem2  46530  ioodvbdlimc1lem2  46533  ioodvbdlimc2lem  46535  stoweidlem3  46604  stoweidlem26  46627  wallispilem1  46666  wallispilem5  46670  stirlinglem1  46675  stirlinglem5  46679  stirlinglem8  46682  stirlinglem10  46684  stirlinglem12  46686  fourierdlem6  46714  fourierdlem7  46715  fourierdlem14  46722  fourierdlem19  46727  fourierdlem35  46743  fourierdlem39  46747  fourierdlem42  46750  fourierdlem50  46757  fourierdlem73  46780  fourierdlem76  46783  fourierdlem77  46784  fourierdlem81  46788  fourierdlem90  46797  fourierdlem92  46799  fourierdlem93  46800  fourierdlem111  46818  fouriersw  46832  etransclem38  46873  sge0split  47010  ovnsslelem  47161  chnsubseq  47483  chnsuslle  47484  chnerlem1  47485  lighneallem4a  48244  rhmsubcALTV  48934  logbpw2m1  49227  dignn0flhalflem1  49275  dignn0flhalflem2  49276  1aryenef  49305  2aryenef  49316  2itscp  49441  amgmwlem  50471