Theorem 3brtr4d 5104

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

Syntax hints:   → wi 4   = wceq 1547   class class class wbr 5072

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073

This theorem is referenced by:  f1oiso2  7296  sucdom2  9127  ordtypelem6  9428  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  fin23lem26  10238  distrnq  10875  lediv12a  12040  recp1lt1  12045  ifle  13140  xleadd1a  13196  xlemul1a  13231  fldiv4p1lem1div2  13785  fldiv4lem1div2  13787  quoremz  13805  quoremnn0ALT  13807  intfracq  13809  modmulnn  13839  fzennn  13921  monoord2  13986  expgt1  14053  expmordi  14120  leexp2r  14127  leexp1a  14128  bernneq  14182  expmulnbnd  14188  digit1  14190  faclbnd  14243  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd6  14252  facubnd  14253  hashdomi  14333  fzsdom2  14381  absrele  15261  absimle  15262  abstri  15284  abs2difabs  15288  limsupval2  15433  rlimrege0  15532  rlimrecl  15533  climsqz  15594  climsqz2  15595  rlimdiv  15599  rlimsqz  15603  rlimsqz2  15604  isercolllem1  15618  isercoll2  15622  fsumcvg2  15680  fsumrlim  15765  o1fsum  15767  cvgcmpce  15772  isumle  15800  climcndslem1  15805  climcndslem2  15806  harmonic  15815  expcnv  15820  explecnv  15821  geomulcvg  15832  efcllem  16033  ege2le3  16046  eflegeo  16079  rpnnen2lem4  16175  ruclem2  16190  ruclem8  16195  fsumdvds  16268  phibnd  16732  iserodd  16797  pcdvdstr  16838  pcprmpw2  16844  pockthg  16868  prmreclem4  16881  prmolefac  17008  2expltfac  17054  mod2ile  18451  pfxchn  18567  chnub  18579  chnccats1  18582  chnccat  18583  chnrev  18584  ex-chn2  18595  odsubdvds  19537  pgpfi  19571  fislw  19591  efgredlemd  19710  efgredlem  19713  frgpcpbl  19725  omndmul  20101  ogrpsub  20103  gsumle  20111  rnghmsubcsetc  20605  rhmsubcsetc  20634  rhmsubcrngc  20640  rhmsubc  20661  abvres  20803  abvtrivd  20804  znrrg  21540  ofldchr  21551  cstucnd  24266  psmetge0  24295  psmetres2  24297  xmetge0  24327  xmetres2  24344  imasf1oxmet  24358  comet  24496  stdbdxmet  24498  dscmet  24555  nrmmetd  24557  nmrtri  24607  tngngp  24637  nmolb2d  24701  nmoleub  24714  nmoco  24720  nmotri  24722  nmoid  24725  nmods  24727  cnmet  24754  xrsxmet  24793  metdstri  24835  metnrmlem3  24845  lebnumlem3  24948  ipcau2  25219  tcphcphlem1  25220  tcphcph  25222  trirn  25385  rrxmet  25393  rrxdstprj1  25394  minveclem2  25411  ovolunlem1a  25481  ovolscalem1  25498  volss  25518  voliunlem1  25535  volcn  25591  itg1climres  25699  mbfi1fseqlem5  25704  mbfi1fseqlem6  25705  itg2const2  25726  itg2seq  25727  itg2mulc  25732  itg2splitlem  25733  itg2monolem1  25735  itg2i1fseqle  25739  itg2i1fseq  25740  itg2i1fseq2  25741  itg2addlem  25743  itg2cnlem1  25746  itg2cnlem2  25747  iblss  25790  itgle  25795  ibladdlem  25805  iblabs  25814  iblabsr  25815  iblmulc2  25816  itgabs  25820  bddmulibl  25824  bddiblnc  25827  dvfsumabs  26008  dvfsumlem2  26012  dvfsum2  26019  deg1suble  26090  deg1mul3le  26100  plyeq0lem  26193  dgrcolem2  26257  geolim3  26323  aaliou3lem2  26327  aaliou3lem8  26329  ulmdvlem1  26383  radcnvlem1  26396  radcnvlem2  26397  dvradcnv  26404  pserulm  26405  pserdvlem2  26411  abelthlem2  26415  abelthlem5  26418  abelthlem7  26421  abelth2  26425  tangtx  26487  tanabsge  26488  tanord1  26519  argregt0  26592  argrege0  26593  argimgt0  26594  abslogle  26600  logcnlem4  26627  logtayllem  26641  abscxpbnd  26735  ang180lem2  26792  atanlogsublem  26897  atans2  26913  leibpi  26924  birthdaylem3  26935  cxplim  26953  cxp2limlem  26957  cxploglim2  26960  jensenlem2  26969  jensen  26970  amgmlem  26971  emcllem2  26978  emcllem4  26980  emcllem7  26983  zetacvg  26996  lgamgulmlem2  27011  lgamgulmlem5  27014  ftalem5  27058  basellem4  27065  basellem6  27067  basellem8  27069  basellem9  27070  chtwordi  27137  chpwordi  27138  ppiwordi  27143  ppiub  27185  vmalelog  27186  chtlepsi  27187  chtleppi  27191  chtublem  27192  chtub  27193  chpub  27201  logfaclbnd  27203  logfacrlim  27205  dchrptlem3  27247  bcmono  27258  bclbnd  27261  bposlem1  27265  bposlem6  27270  bposlem9  27273  lgsqrlem4  27330  2lgslem1c  27374  chebbnd1lem1  27450  chebbnd1lem3  27452  chebbnd1  27453  chtppilimlem1  27454  vmadivsum  27463  rplogsumlem2  27466  dchrisumlema  27469  dchrisumlem3  27472  dchrmusum2  27475  dchrvmasumlem3  27480  dchrvmasumiflem1  27482  dchrisum0flblem1  27489  dchrisum0re  27494  dchrisum0lem2a  27498  mulogsumlem  27512  mulog2sumlem1  27515  mulog2sumlem2  27516  2vmadivsumlem  27521  selberg2lem  27531  selberg3lem1  27538  selberg4lem1  27541  pntrlog2bndlem3  27560  pntrlog2bndlem5  27562  pntrlog2bndlem6  27564  pntpbnd1  27567  pntlemc  27576  pntlemr  27583  pntlemk  27587  pntlemo  27588  abvcxp  27596  ostth2lem1  27599  padicabv  27611  ostth2lem2  27615  ostth2lem3  27616  ostth2lem4  27617  ostth2  27618  noextendlt  27651  noextendgt  27652  nosupbnd1  27696  nosupbnd2lem1  27697  noinfbnd1  27711  noinfbnd2lem1  27712  lltr  27872  addsproplem2  27980  addsproplem4  27982  addsproplem5  27983  addsproplem6  27984  mulsproplem5  28130  mulsproplem6  28131  mulsproplem7  28132  mulsproplem8  28133  lemulsd  28148  mulsuniflem  28159  lemuls1ad  28192  precsexlem9  28225  bdaypw2n0bndlem  28473  legso  28685  trgcopy  28890  eucrct2eupth  30333  nvmtri  30760  imsmetlem  30779  vacn  30783  nmcvcn  30784  smcnlem  30786  blometi  30892  ipblnfi  30944  minvecolem2  30964  hhssnv  31353  nmcoplbi  32117  nmopcoi  32184  nmopcoadji  32190  idleop  32220  cdj1i  32522  isoun  32794  xlt2addrd  32851  nexple  32936  mgcf1o  33082  cycpmconjslem2  33236  archirngz  33270  elrgspnlem1  33323  q1pvsca  33687  lssdimle  33792  fedgmullem2  33814  fldextrspundglemul  33863  extdgfialglem1  33876  fldext2chn  33912  2sqr3minply  33964  cos9thpiminply  33972  pstmxmet  34081  esumpmono  34263  esumcvg  34270  meascnbl  34403  omsmon  34482  omsmeas  34507  dstfrvinc  34661  hgt750lemd  34832  hgt750lema  34841  hgt750leme  34842  swrdwlk  35355  derangenlem  35399  subfaclefac  35404  subfaclim  35416  erdszelem10  35428  sinccvglem  35900  iprodefisum  35969  unbdqndv2lem2  36816  itg2gt0cn  38042  ibladdnclem  38043  iblabsnc  38051  iblmulc2nc  38052  itgabsnc  38056  ftc1anclem7  38066  ftc1anclem8  38067  ftc1anc  38068  mettrifi  38124  equivbnd2  38159  heiborlem6  38183  bfplem1  38189  bfp  38191  rrnmet  38196  rrndstprj1  38197  rrndstprj2  38198  dalawlem3  40365  dalawlem4  40366  dalawlem6  40368  dalawlem9  40371  dalawlem11  40373  dalawlem12  40374  dalawlem15  40377  cdleme3c  40722  cdleme7e  40739  cdleme26e  40851  cdleme26eALTN  40853  cdleme27a  40859  cdleme32c  40935  cdleme32e  40937  cdleme32le  40939  cdlemg9b  41125  cdlemg12b  41136  cdlemg12d  41138  trlcolem  41218  trlcone  41220  cdlemk7  41340  cdlemk7u  41362  cdlemk39  41408  cdlemk11ta  41421  cdlemk11tc  41437  mapdcnvatN  42158  explt1d  42800  frlmvscadiccat  42996  3cubeslem1  43133  irrapxlem5  43271  pell1qrge1  43315  pell1qrgaplem  43318  pell14qrgapw  43321  pellqrex  43324  pellfund14  43343  jm2.17a  43405  jm2.17c  43407  acongeq  43428  jm2.19  43438  jm2.27a  43450  jm2.27c  43452  jm3.1lem2  43463  areaquad  43661  rp-isfinite6  43962  hashnzfzclim  44766  binomcxplemnotnn0  44800  absimlere  45922  monoord2xrv  45926  ltmod  46081  liminflelimsuplem  46218  dvbdfbdioolem2  46372  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  stoweidlem3  46446  stoweidlem26  46469  wallispilem1  46508  wallispilem5  46512  stirlinglem1  46517  stirlinglem5  46521  stirlinglem8  46524  stirlinglem10  46526  stirlinglem12  46528  fourierdlem6  46556  fourierdlem7  46557  fourierdlem14  46564  fourierdlem19  46569  fourierdlem35  46585  fourierdlem39  46589  fourierdlem42  46592  fourierdlem50  46599  fourierdlem73  46622  fourierdlem76  46625  fourierdlem77  46626  fourierdlem81  46630  fourierdlem90  46639  fourierdlem92  46641  fourierdlem93  46642  fourierdlem111  46660  fouriersw  46674  etransclem38  46715  sge0split  46852  ovnsslelem  47003  chnsubseq  47325  chnsuslle  47326  chnerlem1  47327  lighneallem4a  48086  rhmsubcALTV  48776  logbpw2m1  49058  dignn0flhalflem1  49106  dignn0flhalflem2  49107  1aryenef  49136  2aryenef  49147  2itscp  49272  amgmwlem  50292