Theorem 3brtr4d 5145

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112

This theorem is used by:  f1oiso2  7356  sucdom2  9190  ordtypelem6  9488  ttrcltr  9688  ttrclss  9692  ttrclselem2  9698  fin23lem26  10320  distrnq  10957  lediv12a  12119  recp1lt1  12124  ifle  13235  xleadd1a  13291  xlemul1a  13326  fldiv4p1lem1div2  13882  fldiv4lem1div2  13884  quoremz  13902  quoremnn0ALT  13904  intfracq  13906  modmulnn  13936  fzennn  14018  monoord2  14083  expgt1  14150  expmordi  14217  leexp2r  14224  leexp1a  14225  bernneq  14279  expmulnbnd  14285  digit1  14287  faclbnd  14340  faclbnd4lem3  14345  faclbnd4lem4  14346  faclbnd6  14349  facubnd  14350  hashdomi  14430  fzsdom2  14479  absrele  15379  absimle  15380  abstri  15402  abs2difabs  15406  limsupval2  15551  rlimrege0  15650  rlimrecl  15651  climsqz  15712  climsqz2  15713  rlimdiv  15717  rlimsqz  15721  rlimsqz2  15722  isercolllem1  15736  isercoll2  15740  fsumcvg2  15797  fsumrlim  15882  o1fsum  15884  cvgcmpce  15889  isumle  15917  climcndslem1  15922  climcndslem2  15923  harmonic  15932  expcnv  15937  explecnv  15938  geomulcvg  15949  efcllem  16149  ege2le3  16162  eflegeo  16195  rpnnen2lem4  16291  ruclem2  16306  ruclem8  16311  fsumdvds  16384  phibnd  16848  iserodd  16913  pcdvdstr  16954  pcprmpw2  16960  pockthg  16984  prmreclem4  16997  prmolefac  17124  2expltfac  17170  mod2ile  18568  pfxchn  18684  chnub  18696  chnccats1  18699  chnccat  18700  chnrev  18701  ex-chn2  18712  odsubdvds  19665  pgpfi  19699  fislw  19719  efgredlemd  19838  efgredlem  19841  frgpcpbl  19853  omndmul  20229  ogrpsub  20231  gsumle  20239  rnghmsubcsetc  20762  rhmsubcsetc  20791  rhmsubcrngc  20797  rhmsubc  20818  abvres  20964  abvtrivd  20965  znrrg  21745  ofldchr  21756  cstucnd  24471  psmetge0  24500  psmetres2  24502  xmetge0  24532  xmetres2  24549  imasf1oxmet  24563  comet  24701  stdbdxmet  24703  dscmet  24760  nrmmetd  24762  nmrtri  24812  tngngp  24842  nmolb2d  24906  nmoleub  24919  nmoco  24925  nmotri  24927  nmoid  24930  nmods  24932  cnmet  24959  xrsxmet  24998  metdstri  25040  metnrmlem3  25050  lebnumlem3  25153  ipcau2  25424  tcphcphlem1  25425  tcphcph  25427  trirn  25590  rrxmet  25598  rrxdstprj1  25599  minveclem2  25616  ovolunlem1a  25686  ovolscalem1  25703  volss  25723  voliunlem1  25740  volcn  25796  itg1climres  25904  mbfi1fseqlem5  25909  mbfi1fseqlem6  25910  itg2const2  25931  itg2seq  25932  itg2mulc  25937  itg2splitlem  25938  itg2monolem1  25940  itg2i1fseqle  25944  itg2i1fseq  25945  itg2i1fseq2  25946  itg2addlem  25948  itg2cnlem1  25951  itg2cnlem2  25952  iblss  25995  itgle  26000  ibladdlem  26010  iblabs  26019  iblabsr  26020  iblmulc2  26021  itgabs  26025  bddmulibl  26029  bddiblnc  26032  dvfsumabs  26213  dvfsumlem2  26217  dvfsum2  26224  deg1suble  26295  deg1mul3le  26305  plyeq0lem  26398  dgrcolem2  26462  geolim3  26533  aaliou3lem2  26537  aaliou3lem8  26539  ulmdvlem1  26594  radcnvlem1  26607  radcnvlem2  26608  dvradcnv  26615  pserulm  26616  pserdvlem2  26622  abelthlem2  26626  abelthlem5  26629  abelthlem7  26632  abelth2  26636  tangtx  26701  tanabsge  26702  tanord1  26733  argregt0  26806  argrege0  26807  argimgt0  26808  abslogle  26814  logcnlem4  26841  logtayllem  26855  abscxpbnd  26949  ang180lem2  27006  atanlogsublem  27111  atans2  27127  leibpi  27138  birthdaylem3  27149  cxplim  27167  cxp2limlem  27171  cxploglim2  27174  jensenlem2  27183  jensen  27184  amgmlem  27185  emcllem2  27192  emcllem4  27194  emcllem7  27197  zetacvg  27210  lgamgulmlem2  27225  lgamgulmlem5  27228  ftalem5  27272  basellem4  27279  basellem6  27281  basellem8  27283  basellem9  27284  chtwordi  27351  chpwordi  27352  ppiwordi  27357  ppiub  27399  vmalelog  27400  chtlepsi  27401  chtleppi  27405  chtublem  27406  chtub  27407  chpub  27415  logfaclbnd  27417  logfacrlim  27419  dchrptlem3  27461  bcmono  27472  bclbnd  27475  bposlem1  27479  bposlem6  27484  bposlem9  27487  lgsqrlem4  27544  2lgslem1c  27588  chebbnd1lem1  27664  chebbnd1lem3  27666  chebbnd1  27667  chtppilimlem1  27668  vmadivsum  27677  rplogsumlem2  27680  dchrisumlema  27683  dchrisumlem3  27686  dchrmusum2  27689  dchrvmasumlem3  27694  dchrvmasumiflem1  27696  dchrisum0flblem1  27703  dchrisum0re  27708  dchrisum0lem2a  27712  mulogsumlem  27726  mulog2sumlem1  27729  mulog2sumlem2  27730  2vmadivsumlem  27735  selberg2lem  27745  selberg3lem1  27752  selberg4lem1  27755  pntrlog2bndlem3  27774  pntrlog2bndlem5  27776  pntrlog2bndlem6  27778  pntpbnd1  27781  pntlemc  27790  pntlemr  27797  pntlemk  27801  pntlemo  27802  abvcxp  27810  ostth2lem1  27813  padicabv  27825  ostth2lem2  27829  ostth2lem3  27830  ostth2lem4  27831  ostth2  27832  noextendlt  27864  noextendgt  27865  nosupbnd1  27909  nosupbnd2lem1  27910  noinfbnd1  27924  noinfbnd2lem1  27925  lltr  28086  addsproplem2  28194  addsproplem4  28196  addsproplem5  28197  addsproplem6  28198  mulsproplem5  28344  mulsproplem6  28345  mulsproplem7  28346  mulsproplem8  28347  lemulsd  28362  mulsuniflem  28373  lemuls1ad  28406  precsexlem9  28439  bdaypw2n0bndlem  28687  legso  28899  trgcopy  29146  swrdwlk  30071  eucrct2eupth  30643  nvmtri  31070  imsmetlem  31089  vacn  31093  nmcvcn  31094  smcnlem  31096  blometi  31202  ipblnfi  31254  minvecolem2  31274  hhssnv  31663  nmcoplbi  32427  nmopcoi  32494  nmopcoadji  32500  idleop  32530  cdj1i  32832  isoun  33094  xlt2addrd  33150  nexple  33223  mgcf1o  33363  cycpmconjslem2  33515  archirngz  33549  elrgspnlem1  33602  q1pvsca  33934  lssdimle  34038  fedgmullem2  34060  fldextrspundglemul  34109  extdgfialglem1  34122  fldext2chn  34158  2sqr3minply  34210  cos9thpiminply  34218  pstmxmet  34327  esumpmono  34509  esumcvg  34516  meascnbl  34650  omsmon  34729  omsmeas  34754  dstfrvinc  34908  hgt750lemd  35076  hgt750lema  35085  hgt750leme  35086  derangenlem  35676  subfaclefac  35681  subfaclim  35693  erdszelem10  35705  sinccvglem  36177  iprodefisum  36246  unbdqndv2lem2  37132  itg2gt0cn  38359  ibladdnclem  38360  iblabsnc  38368  iblmulc2nc  38369  itgabsnc  38373  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  mettrifi  38441  equivbnd2  38476  heiborlem6  38500  bfplem1  38506  bfp  38508  rrnmet  38513  rrndstprj1  38514  rrndstprj2  38515  dalawlem3  40680  dalawlem4  40681  dalawlem6  40683  dalawlem9  40686  dalawlem11  40688  dalawlem12  40689  dalawlem15  40692  cdleme3c  41037  cdleme7e  41054  cdleme26e  41166  cdleme26eALTN  41168  cdleme27a  41174  cdleme32c  41250  cdleme32e  41252  cdleme32le  41254  cdlemg9b  41440  cdlemg12b  41451  cdlemg12d  41453  trlcolem  41533  trlcone  41535  cdlemk7  41655  cdlemk7u  41677  cdlemk39  41723  cdlemk11ta  41736  cdlemk11tc  41752  mapdcnvatN  42473  explt1d  43117  frlmvscadiccat  43313  3cubeslem1  43448  irrapxlem5  43586  pell1qrge1  43630  pell1qrgaplem  43633  pell14qrgapw  43636  pellqrex  43639  pellfund14  43658  jm2.17a  43720  jm2.17c  43722  acongeq  43743  jm2.19  43753  jm2.27a  43765  jm2.27c  43767  jm3.1lem2  43778  areaquad  43976  rp-isfinite6  44277  hashnzfzclim  45065  binomcxplemnotnn0  45099  absimlere  46226  monoord2xrv  46230  ltmod  46385  liminflelimsuplem  46522  dvbdfbdioolem2  46676  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  stoweidlem3  46750  stoweidlem26  46773  wallispilem1  46812  wallispilem5  46816  stirlinglem1  46821  stirlinglem5  46825  stirlinglem8  46828  stirlinglem10  46830  stirlinglem12  46832  fourierdlem6  46860  fourierdlem7  46861  fourierdlem14  46868  fourierdlem19  46873  fourierdlem35  46889  fourierdlem39  46893  fourierdlem42  46896  fourierdlem50  46903  fourierdlem73  46926  fourierdlem76  46929  fourierdlem77  46930  fourierdlem81  46934  fourierdlem90  46943  fourierdlem92  46945  fourierdlem93  46946  fourierdlem111  46964  fouriersw  46978  etransclem38  47019  sge0split  47156  ovnsslelem  47307  chnsubseq  47629  chnsuslle  47630  chnerlem1  47631  lighneallem4a  48393  rhmsubcALTV  49083  logbpw2m1  49380  dignn0flhalflem1  49428  dignn0flhalflem2  49429  1aryenef  49458  2aryenef  49469  2itscp  49594  amgmwlem  50683