Theorem 3brtr4d 5137

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  f1oiso2  7353  sucdom2  9197  ordtypelem6  9495  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  fin23lem26  10327  distrnq  10970  lediv12a  12132  recp1lt1  12137  ifle  13249  xleadd1a  13305  xlemul1a  13340  fldiv4p1lem1div2  13896  fldiv4lem1div2  13898  quoremz  13916  quoremnn0ALT  13918  intfracq  13920  modmulnn  13950  fzennn  14032  monoord2  14097  expgt1  14164  expmordi  14231  leexp2r  14238  leexp1a  14239  bernneq  14293  expmulnbnd  14299  digit1  14301  faclbnd  14354  faclbnd4lem3  14359  faclbnd4lem4  14360  faclbnd6  14363  facubnd  14364  hashdomi  14444  fzsdom2  14493  absrele  15395  absimle  15396  abstri  15418  abs2difabs  15422  limsupval2  15567  rlimrege0  15666  rlimrecl  15667  climsqz  15728  climsqz2  15729  rlimdiv  15733  rlimsqz  15737  rlimsqz2  15738  isercolllem1  15752  isercoll2  15756  fsumcvg2  15813  fsumrlim  15898  o1fsum  15900  cvgcmpce  15905  isumle  15933  climcndslem1  15938  climcndslem2  15939  harmonic  15948  expcnv  15953  explecnv  15954  geomulcvg  15965  efcllem  16163  ege2le3  16176  eflegeo  16209  rpnnen2lem4  16305  ruclem2  16320  ruclem8  16325  fsumdvds  16398  phibnd  16862  iserodd  16927  pcdvdstr  16968  pcprmpw2  16974  pockthg  16998  prmreclem4  17011  prmolefac  17138  2expltfac  17184  mod2ile  18582  pfxchn  18698  chnub  18710  chnccats1  18713  chnccat  18714  chnrev  18715  ex-chn2  18726  odsubdvds  19698  pgpfi  19732  fislw  19752  efgredlemd  19871  efgredlem  19874  frgpcpbl  19886  omndmul  20262  ogrpsub  20264  gsumle  20272  rnghmsubcsetc  20795  rhmsubcsetc  20824  rhmsubcrngc  20830  rhmsubc  20851  abvres  20997  abvtrivd  20998  znrrg  21778  ofldchr  21789  cstucnd  24509  psmetge0  24538  psmetres2  24540  xmetge0  24570  xmetres2  24587  imasf1oxmet  24601  comet  24739  stdbdxmet  24741  dscmet  24798  nrmmetd  24800  nmrtri  24850  tngngp  24880  nmolb2d  24944  nmoleub  24957  nmoco  24963  nmotri  24965  nmoid  24968  nmods  24970  cnmet  24997  xrsxmet  25036  metdstri  25078  metnrmlem3  25088  lebnumlem3  25191  ipcau2  25462  tcphcphlem1  25463  tcphcph  25465  trirn  25628  rrxmet  25636  rrxdstprj1  25637  minveclem2  25654  ovolunlem1a  25724  ovolscalem1  25741  volss  25761  voliunlem1  25778  volcn  25834  itg1climres  25942  mbfi1fseqlem5  25947  mbfi1fseqlem6  25948  itg2const2  25969  itg2seq  25970  itg2mulc  25975  itg2splitlem  25976  itg2monolem1  25978  itg2i1fseqle  25982  itg2i1fseq  25983  itg2i1fseq2  25984  itg2addlem  25986  itg2cnlem1  25989  itg2cnlem2  25990  iblss  26032  itgle  26037  ibladdlem  26047  iblabs  26056  iblabsr  26057  iblmulc2  26058  itgabs  26062  bddmulibl  26066  bddiblnc  26069  dvfsumabs  26250  dvfsumlem2  26254  dvfsum2  26261  deg1suble  26332  deg1mul3le  26342  plyeq0lem  26436  dgrcolem2  26500  geolim3  26575  aaliou3lem2  26579  aaliou3lem8  26581  ulmdvlem1  26636  radcnvlem1  26649  radcnvlem2  26650  dvradcnv  26657  pserulm  26658  pserdvlem2  26664  abelthlem2  26668  abelthlem5  26671  abelthlem7  26674  abelth2  26678  tangtx  26743  tanabsge  26744  tanord1  26774  argregt0  26847  argrege0  26848  argimgt0  26849  abslogle  26855  logcnlem4  26882  logtayllem  26896  abscxpbnd  26990  ang180lem2  27047  atanlogsublem  27152  atans2  27168  leibpi  27179  birthdaylem3  27190  cxplim  27208  cxp2limlem  27212  cxploglim2  27215  jensenlem2  27224  jensen  27225  amgmlem  27226  emcllem2  27233  emcllem4  27235  emcllem7  27238  zetacvg  27251  lgamgulmlem2  27266  lgamgulmlem5  27269  ftalem5  27313  basellem4  27320  basellem6  27322  basellem8  27324  basellem9  27325  chtwordi  27392  chpwordi  27393  ppiwordi  27398  ppiub  27440  vmalelog  27441  chtlepsi  27442  chtleppi  27446  chtublem  27447  chtub  27448  chpub  27456  logfaclbnd  27458  logfacrlim  27460  dchrptlem3  27502  bcmono  27513  bclbnd  27516  bposlem1  27520  bposlem6  27525  bposlem9  27528  lgsqrlem4  27585  2lgslem1c  27629  chebbnd1lem1  27705  chebbnd1lem3  27707  chebbnd1  27708  chtppilimlem1  27709  vmadivsum  27718  rplogsumlem2  27721  dchrisumlema  27724  dchrisumlem3  27727  dchrmusum2  27730  dchrvmasumlem3  27735  dchrvmasumiflem1  27737  dchrisum0flblem1  27744  dchrisum0re  27749  dchrisum0lem2a  27753  mulogsumlem  27767  mulog2sumlem1  27770  mulog2sumlem2  27771  2vmadivsumlem  27776  selberg2lem  27786  selberg3lem1  27793  selberg4lem1  27796  pntrlog2bndlem3  27815  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntpbnd1  27822  pntlemc  27831  pntlemr  27838  pntlemk  27842  pntlemo  27843  abvcxp  27851  ostth2lem1  27854  padicabv  27866  ostth2lem2  27870  ostth2lem3  27871  ostth2lem4  27872  ostth2  27873  noextendlt  27905  noextendgt  27906  nosupbnd1  27950  nosupbnd2lem1  27951  noinfbnd1  27965  noinfbnd2lem1  27966  lltr  28127  addsproplem2  28235  addsproplem4  28237  addsproplem5  28238  addsproplem6  28239  mulsproplem5  28385  mulsproplem6  28386  mulsproplem7  28387  mulsproplem8  28388  lemulsd  28403  mulsuniflem  28414  lemuls1ad  28447  precsexlem9  28480  bdaypw2n0bndlem  28728  legso  28941  trgcopy  29190  cgraer  29256  angmgmaddov1  29267  angmgmaddov2  29268  swrdwlk  30147  eucrct2eupth  30725  nvmtri  31152  imsmetlem  31171  vacn  31175  nmcvcn  31176  smcnlem  31178  blometi  31284  ipblnfi  31336  minvecolem2  31356  hhssnv  31745  nmcoplbi  32509  nmopcoi  32576  nmopcoadji  32582  idleop  32612  cdj1i  32914  isoun  33174  xlt2addrd  33230  nexple  33303  mgcf1o  33443  cycpmconjslem2  33595  archirngz  33629  elrgspnlem1  33682  q1pvsca  34014  lssdimle  34118  fedgmullem2  34140  fldextrspundglemul  34189  extdgfialglem1  34202  fldext2chn  34238  2sqr3minply  34290  cos9thpiminply  34298  pstmxmet  34407  esumpmono  34589  esumcvg  34596  meascnbl  34730  omsmon  34809  omsmeas  34834  dstfrvinc  34988  hgt750lemd  35156  hgt750lema  35165  hgt750leme  35166  derangenlem  35750  subfaclefac  35755  subfaclim  35767  erdszelem10  35779  sinccvglem  36251  iprodefisum  36320  unbdqndv2lem2  37207  itg2gt0cn  38424  ibladdnclem  38425  iblabsnc  38433  iblmulc2nc  38434  itgabsnc  38438  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  mettrifi  38507  equivbnd2  38542  heiborlem6  38566  bfplem1  38572  bfp  38574  rrnmet  38579  rrndstprj1  38580  rrndstprj2  38581  dalawlem3  40746  dalawlem4  40747  dalawlem6  40749  dalawlem9  40752  dalawlem11  40754  dalawlem12  40755  dalawlem15  40758  cdleme3c  41103  cdleme7e  41120  cdleme26e  41232  cdleme26eALTN  41234  cdleme27a  41240  cdleme32c  41316  cdleme32e  41318  cdleme32le  41320  cdlemg9b  41506  cdlemg12b  41517  cdlemg12d  41519  trlcolem  41599  trlcone  41601  cdlemk7  41721  cdlemk7u  41743  cdlemk39  41789  cdlemk11ta  41802  cdlemk11tc  41818  mapdcnvatN  42539  explt1d  43198  frlmvscadiccat  43394  3cubeslem1  43529  irrapxlem5  43667  pell1qrge1  43711  pell1qrgaplem  43714  pell14qrgapw  43717  pellqrex  43720  pellfund14  43739  jm2.17a  43801  jm2.17c  43803  acongeq  43824  jm2.19  43834  jm2.27a  43846  jm2.27c  43848  jm3.1lem2  43859  areaquad  44057  rp-isfinite6  44358  hashnzfzclim  45146  binomcxplemnotnn0  45180  absimlere  46307  monoord2xrv  46311  ltmod  46466  liminflelimsuplem  46603  dvbdfbdioolem2  46757  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  stoweidlem3  46831  stoweidlem26  46854  wallispilem1  46893  wallispilem5  46897  stirlinglem1  46902  stirlinglem5  46906  stirlinglem8  46909  stirlinglem10  46911  stirlinglem12  46913  fourierdlem6  46941  fourierdlem7  46942  fourierdlem14  46949  fourierdlem19  46954  fourierdlem35  46970  fourierdlem39  46974  fourierdlem42  46977  fourierdlem50  46984  fourierdlem73  47007  fourierdlem76  47010  fourierdlem77  47011  fourierdlem81  47015  fourierdlem90  47024  fourierdlem92  47026  fourierdlem93  47027  fourierdlem111  47045  fouriersw  47059  etransclem38  47100  sge0split  47237  ovnsslelem  47388  chnsubseq  47708  chnsuslle  47709  chnerlem1  47710  lighneallem4a  48511  rhmsubcALTV  49200  logbpw2m1  49497  dignn0flhalflem1  49545  dignn0flhalflem2  49546  1aryenef  49575  2aryenef  49586  2itscp  49711  amgmwlem  50820