Theorem 3brtr4d 5136

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 260	1 ⊢ (𝜑 → 𝐶𝑅𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   class class class wbr 5102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103

This theorem is used by:  f1oiso2  7364  sucdom2  9225  ordtypelem6  9524  ttrcltr  9724  ttrclss  9728  ttrclselem2  9734  fin23lem26  10410  distrnq  11053  lediv12a  12217  recp1lt1  12222  ifle  13334  xleadd1a  13390  xlemul1a  13425  fldiv4p1lem1div2  13982  fldiv4lem1div2  13984  quoremz  14002  quoremnn0ALT  14004  intfracq  14006  modmulnn  14036  fzennn  14118  monoord2  14183  expgt1  14250  expmordi  14317  leexp2r  14324  leexp1a  14325  bernneq  14380  expmulnbnd  14386  digit1  14388  faclbnd  14441  faclbnd4lem3  14446  faclbnd4lem4  14447  faclbnd6  14450  facubnd  14451  hashdomi  14531  fzsdom2  14580  absrele  15484  absimle  15485  abstri  15507  abs2difabs  15511  limsupval2  15656  rlimrege0  15755  rlimrecl  15756  climsqz  15817  climsqz2  15818  rlimdiv  15822  rlimsqz  15826  rlimsqz2  15827  isercolllem1  15841  isercoll2  15845  fsumcvg2  15902  fsumrlim  15987  o1fsum  15989  cvgcmpce  15994  isumle  16022  climcndslem1  16027  climcndslem2  16028  harmonic  16037  expcnv  16042  explecnv  16043  geomulcvg  16054  efcllem  16252  ege2le3  16265  eflegeo  16298  rpnnen2lem4  16394  ruclem2  16409  ruclem8  16414  fsumdvds  16487  phibnd  16957  iserodd  17022  pcdvdstr  17063  pcprmpw2  17069  pockthg  17093  prmreclem4  17106  prmolefac  17233  2expltfac  17279  mod2ile  18677  pfxchn  18793  chnub  18805  chnccats1  18808  chnccat  18809  chnrev  18810  ex-chn2  18821  odsubdvds  19794  pgpfi  19828  fislw  19848  efgredlemd  19967  efgredlem  19970  frgpcpbl  19982  omndmul  20358  ogrpsub  20360  gsumle  20368  rnghmsubcsetc  20894  rhmsubcsetc  20923  rhmsubcrngc  20929  rhmsubc  20950  abvres  21097  abvtrivd  21098  znrrg  21880  ofldchr  21891  cstucnd  24611  psmetge0  24640  psmetres2  24642  xmetge0  24672  xmetres2  24689  imasf1oxmet  24703  comet  24841  stdbdxmet  24843  dscmet  24900  nrmmetd  24902  nmrtri  24952  tngngp  24982  nmolb2d  25046  nmoleub  25059  nmoco  25065  nmotri  25067  nmoid  25070  nmods  25072  cnmet  25099  xrsxmet  25138  metdstri  25180  metnrmlem3  25190  lebnumlem3  25293  ipcau2  25564  tcphcphlem1  25565  tcphcph  25567  trirn  25730  rrxmet  25738  rrxdstprj1  25739  minveclem2  25756  ovolunlem1a  25826  ovolscalem1  25843  volss  25863  voliunlem1  25880  volcn  25936  itg1climres  26044  mbfi1fseqlem5  26049  mbfi1fseqlem6  26050  itg2const2  26071  itg2seq  26072  itg2mulc  26077  itg2splitlem  26078  itg2monolem1  26080  itg2i1fseqle  26084  itg2i1fseq  26085  itg2i1fseq2  26086  itg2addlem  26088  itg2cnlem1  26091  itg2cnlem2  26092  iblss  26134  itgle  26139  ibladdlem  26149  iblabs  26158  iblabsr  26159  iblmulc2  26160  itgabs  26164  bddmulibl  26168  bddiblnc  26171  dvfsumabs  26352  dvfsumlem2  26356  dvfsum2  26363  deg1suble  26434  deg1mul3le  26444  plyeq0lem  26538  dgrcolem2  26602  geolim3  26675  aaliou3lem2  26679  aaliou3lem8  26681  ulmdvlem1  26736  radcnvlem1  26749  radcnvlem2  26750  dvradcnv  26757  pserulm  26758  pserdvlem2  26764  abelthlem2  26768  abelthlem5  26771  abelthlem7  26774  abelth2  26778  tangtx  26843  tanabsge  26844  tanord1  26874  argregt0  26947  argrege0  26948  argimgt0  26949  abslogle  26955  logcnlem4  26982  logtayllem  26996  abscxpbnd  27090  ang180lem2  27147  atanlogsublem  27252  atans2  27268  leibpi  27279  birthdaylem3  27290  cxplim  27308  cxp2limlem  27312  cxploglim2  27315  jensenlem2  27324  jensen  27325  amgmlem  27326  emcllem2  27333  emcllem4  27335  emcllem7  27338  zetacvg  27351  lgamgulmlem2  27366  lgamgulmlem5  27369  ftalem5  27413  basellem4  27420  basellem6  27422  basellem8  27424  basellem9  27425  chtwordi  27492  chpwordi  27493  ppiwordi  27498  ppiub  27540  vmalelog  27541  chtlepsi  27542  chtleppi  27546  chtublem  27547  chtub  27548  chpub  27556  logfaclbnd  27558  logfacrlim  27560  dchrptlem3  27602  bcmono  27613  bclbnd  27616  bposlem1  27620  bposlem6  27625  bposlem9  27628  lgsqrlem4  27685  2lgslem1c  27729  chebbnd1lem1  27805  chebbnd1lem3  27807  chebbnd1  27808  chtppilimlem1  27809  vmadivsum  27818  rplogsumlem2  27821  dchrisumlema  27824  dchrisumlem3  27827  dchrmusum2  27830  dchrvmasumlem3  27835  dchrvmasumiflem1  27837  dchrisum0flblem1  27844  dchrisum0re  27849  dchrisum0lem2a  27853  mulogsumlem  27867  mulog2sumlem1  27870  mulog2sumlem2  27871  2vmadivsumlem  27876  selberg2lem  27886  selberg3lem1  27893  selberg4lem1  27896  pntrlog2bndlem3  27915  pntrlog2bndlem5  27917  pntrlog2bndlem6  27919  pntpbnd1  27922  pntlemc  27931  pntlemr  27938  pntlemk  27942  pntlemo  27943  abvcxp  27951  ostth2lem1  27954  padicabv  27966  ostth2lem2  27970  ostth2lem3  27971  ostth2lem4  27972  ostth2  27973  noextendlt  28035  noextendgt  28036  nosupbnd1  28080  nosupbnd2lem1  28081  noinfbnd1  28095  noinfbnd2lem1  28096  lltr  28257  addsproplem2  28365  addsproplem4  28367  addsproplem5  28368  addsproplem6  28369  mulsproplem5  28515  mulsproplem6  28516  mulsproplem7  28517  mulsproplem8  28518  lemulsd  28533  mulsuniflem  28544  lemuls1ad  28577  precsexlem9  28610  bdaypw2n0bndlem  28858  legso  29071  trgcopy  29320  cgraer  29386  angmgmaddov1  29397  angmgmaddov2  29398  swrdwlk  30277  eucrct2eupth  30855  nvmtri  31282  imsmetlem  31301  vacn  31305  nmcvcn  31306  smcnlem  31308  blometi  31414  ipblnfi  31466  minvecolem2  31486  hhssnv  31875  nmcoplbi  32639  nmopcoi  32706  nmopcoadji  32712  idleop  32742  cdj1i  33044  isoun  33346  xlt2addrd  33401  nexple  33474  mgcf1o  33614  cycpmconjslem2  33766  archirngz  33800  elrgspnlem1  33853  q1pvsca  34186  lssdimle  34290  fedgmullem2  34312  fldextrspundglemul  34361  extdgfialglem1  34374  fldext2chn  34410  2sqr3minply  34462  cos9thpiminply  34470  pstmxmet  34579  esumpmono  34761  esumcvg  34768  meascnbl  34902  omsmon  34980  omsmeas  35005  dstfrvinc  35159  hgt750lemd  35327  hgt750lema  35336  hgt750leme  35337  derangenlem  36026  subfaclefac  36031  subfaclim  36043  erdszelem10  36055  sinccvglem  36527  iprodefisum  36602  unbdqndv2lem2  37472  itg2gt0cn  38702  ibladdnclem  38703  iblabsnc  38711  iblmulc2nc  38712  itgabsnc  38716  ftc1anclem7  38726  ftc1anclem8  38727  ftc1anc  38728  mettrifi  38800  equivbnd2  38835  heiborlem6  38859  bfplem1  38865  bfp  38867  rrnmet  38872  rrndstprj1  38873  rrndstprj2  38874  dalawlem3  41039  dalawlem4  41040  dalawlem6  41042  dalawlem9  41045  dalawlem11  41047  dalawlem12  41048  dalawlem15  41051  cdleme3c  41396  cdleme7e  41413  cdleme26e  41525  cdleme26eALTN  41527  cdleme27a  41533  cdleme32c  41609  cdleme32e  41611  cdleme32le  41613  cdlemg9b  41799  cdlemg12b  41810  cdlemg12d  41812  trlcolem  41892  trlcone  41894  cdlemk7  42014  cdlemk7u  42036  cdlemk39  42082  cdlemk11ta  42095  cdlemk11tc  42111  mapdcnvatN  42832  explt1d  43489  frlmvscadiccat  43682  3cubeslem1  43803  irrapxlem5  43942  pell1qrge1  43986  pell1qrgaplem  43989  pell14qrgapw  43992  pellqrex  43995  pellfund14  44014  jm2.17a  44076  jm2.17c  44078  acongeq  44099  jm2.19  44109  jm2.27a  44121  jm2.27c  44123  jm3.1lem2  44134  areaquad  44327  rp-isfinite6  44628  hashnzfzclim  45415  binomcxplemnotnn0  45449  absimlere  46597  monoord2xrv  46601  ltmod  46756  liminflelimsuplem  46893  dvbdfbdioolem2  47047  ioodvbdlimc1lem2  47050  ioodvbdlimc2lem  47052  stoweidlem3  47121  stoweidlem26  47144  wallispilem1  47183  wallispilem5  47187  stirlinglem1  47192  stirlinglem5  47196  stirlinglem8  47199  stirlinglem10  47201  stirlinglem12  47203  fourierdlem6  47231  fourierdlem7  47232  fourierdlem14  47239  fourierdlem19  47244  fourierdlem35  47260  fourierdlem39  47264  fourierdlem42  47267  fourierdlem50  47274  fourierdlem73  47297  fourierdlem76  47300  fourierdlem77  47301  fourierdlem81  47305  fourierdlem90  47314  fourierdlem92  47316  fourierdlem93  47317  fourierdlem111  47335  fouriersw  47349  etransclem38  47390  sge0split  47527  ovnsslelem  47678  chnsubseq  47998  chnsuslle  47999  chnerlem1  48000  lighneallem4a  48801  rhmsubcALTV  49490  logbpw2m1  49787  dignn0flhalflem1  49835  dignn0flhalflem2  49836  1aryenef  49865  2aryenef  49876  2itscp  50001  amgmwlem  51170