Theorem 3brtr4d 5127

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  f1oiso2  7295  sucdom2  9123  ordtypelem6  9420  ttrcltr  9617  ttrclss  9621  ttrclselem2  9627  fin23lem26  10227  distrnq  10863  lediv12a  12026  recp1lt1  12031  ifle  13103  xleadd1a  13159  xlemul1a  13194  fldiv4p1lem1div2  13746  fldiv4lem1div2  13748  quoremz  13766  quoremnn0ALT  13768  intfracq  13770  modmulnn  13800  fzennn  13882  monoord2  13947  expgt1  14014  expmordi  14081  leexp2r  14088  leexp1a  14089  bernneq  14143  expmulnbnd  14149  digit1  14151  faclbnd  14204  faclbnd4lem3  14209  faclbnd4lem4  14210  faclbnd6  14213  facubnd  14214  hashdomi  14294  fzsdom2  14342  absrele  15222  absimle  15223  abstri  15245  abs2difabs  15249  limsupval2  15394  rlimrege0  15493  rlimrecl  15494  climsqz  15555  climsqz2  15556  rlimdiv  15560  rlimsqz  15564  rlimsqz2  15565  isercolllem1  15579  isercoll2  15583  fsumcvg2  15641  fsumrlim  15725  o1fsum  15727  cvgcmpce  15732  isumle  15758  climcndslem1  15763  climcndslem2  15764  harmonic  15773  expcnv  15778  explecnv  15779  geomulcvg  15790  efcllem  15991  ege2le3  16004  eflegeo  16037  rpnnen2lem4  16133  ruclem2  16148  ruclem8  16153  fsumdvds  16226  phibnd  16689  iserodd  16754  pcdvdstr  16795  pcprmpw2  16801  pockthg  16825  prmreclem4  16838  prmolefac  16965  2expltfac  17011  mod2ile  18408  pfxchn  18524  chnub  18536  chnccats1  18539  chnccat  18540  chnrev  18541  ex-chn2  18552  odsubdvds  19491  pgpfi  19525  fislw  19545  efgredlemd  19664  efgredlem  19667  frgpcpbl  19679  omndmul  20055  ogrpsub  20057  gsumle  20065  rnghmsubcsetc  20557  rhmsubcsetc  20586  rhmsubcrngc  20592  rhmsubc  20613  abvres  20755  abvtrivd  20756  znrrg  21511  ofldchr  21522  cstucnd  24218  psmetge0  24247  psmetres2  24249  xmetge0  24279  xmetres2  24296  imasf1oxmet  24310  comet  24448  stdbdxmet  24450  dscmet  24507  nrmmetd  24509  nmrtri  24559  tngngp  24589  nmolb2d  24653  nmoleub  24666  nmoco  24672  nmotri  24674  nmoid  24677  nmods  24679  cnmet  24706  xrsxmet  24745  metdstri  24787  metnrmlem3  24797  lebnumlem3  24909  ipcau2  25181  tcphcphlem1  25182  tcphcph  25184  trirn  25347  rrxmet  25355  rrxdstprj1  25356  minveclem2  25373  ovolunlem1a  25444  ovolscalem1  25461  volss  25481  voliunlem1  25498  volcn  25554  itg1climres  25662  mbfi1fseqlem5  25667  mbfi1fseqlem6  25668  itg2const2  25689  itg2seq  25690  itg2mulc  25695  itg2splitlem  25696  itg2monolem1  25698  itg2i1fseqle  25702  itg2i1fseq  25703  itg2i1fseq2  25704  itg2addlem  25706  itg2cnlem1  25709  itg2cnlem2  25710  iblss  25753  itgle  25758  ibladdlem  25768  iblabs  25777  iblabsr  25778  iblmulc2  25779  itgabs  25783  bddmulibl  25787  bddiblnc  25790  dvfsumabs  25976  dvfsumlem2  25980  dvfsumlem2OLD  25981  dvfsum2  25988  deg1suble  26059  deg1mul3le  26069  plyeq0lem  26162  dgrcolem2  26227  geolim3  26294  aaliou3lem2  26298  aaliou3lem8  26300  ulmdvlem1  26356  radcnvlem1  26369  radcnvlem2  26370  dvradcnv  26377  pserulm  26378  pserdvlem2  26385  abelthlem2  26389  abelthlem5  26392  abelthlem7  26395  abelth2  26399  tangtx  26461  tanabsge  26462  tanord1  26493  argregt0  26566  argrege0  26567  argimgt0  26568  abslogle  26574  logcnlem4  26601  logtayllem  26615  abscxpbnd  26710  ang180lem2  26767  atanlogsublem  26872  atans2  26888  leibpi  26899  birthdaylem3  26910  cxplim  26929  cxp2limlem  26933  cxploglim2  26936  jensenlem2  26945  jensen  26946  amgmlem  26947  emcllem2  26954  emcllem4  26956  emcllem7  26959  zetacvg  26972  lgamgulmlem2  26987  lgamgulmlem5  26990  ftalem5  27034  basellem4  27041  basellem6  27043  basellem8  27045  basellem9  27046  chtwordi  27113  chpwordi  27114  ppiwordi  27119  ppiub  27162  vmalelog  27163  chtlepsi  27164  chtleppi  27168  chtublem  27169  chtub  27170  chpub  27178  logfaclbnd  27180  logfacrlim  27182  dchrptlem3  27224  bcmono  27235  bclbnd  27238  bposlem1  27242  bposlem6  27247  bposlem9  27250  lgsqrlem4  27307  2lgslem1c  27351  chebbnd1lem1  27427  chebbnd1lem3  27429  chebbnd1  27430  chtppilimlem1  27431  vmadivsum  27440  rplogsumlem2  27443  dchrisumlema  27446  dchrisumlem3  27449  dchrmusum2  27452  dchrvmasumlem3  27457  dchrvmasumiflem1  27459  dchrisum0flblem1  27466  dchrisum0re  27471  dchrisum0lem2a  27475  mulogsumlem  27489  mulog2sumlem1  27492  mulog2sumlem2  27493  2vmadivsumlem  27498  selberg2lem  27508  selberg3lem1  27515  selberg4lem1  27518  pntrlog2bndlem3  27537  pntrlog2bndlem5  27539  pntrlog2bndlem6  27541  pntpbnd1  27544  pntlemc  27553  pntlemr  27560  pntlemk  27564  pntlemo  27565  abvcxp  27573  ostth2lem1  27576  padicabv  27588  ostth2lem2  27592  ostth2lem3  27593  ostth2lem4  27594  ostth2  27595  noextendlt  27628  noextendgt  27629  nosupbnd1  27673  nosupbnd2lem1  27674  noinfbnd1  27688  noinfbnd2lem1  27689  lltropt  27837  addsproplem2  27933  addsproplem4  27935  addsproplem5  27936  addsproplem6  27937  mulsproplem5  28079  mulsproplem6  28080  mulsproplem7  28081  mulsproplem8  28082  slemuld  28097  mulsuniflem  28108  slemul1ad  28141  precsexlem9  28173  legso  28597  trgcopy  28802  eucrct2eupth  30246  nvmtri  30672  imsmetlem  30691  vacn  30695  nmcvcn  30696  smcnlem  30698  blometi  30804  ipblnfi  30856  minvecolem2  30876  hhssnv  31265  nmcoplbi  32029  nmopcoi  32096  nmopcoadji  32102  idleop  32132  cdj1i  32434  isoun  32707  xlt2addrd  32767  nexple  32853  mgcf1o  33013  cycpmconjslem2  33165  archirngz  33199  elrgspnlem1  33252  q1pvsca  33613  lssdimle  33692  fedgmullem2  33715  fldextrspundglemul  33764  extdgfialglem1  33777  fldext2chn  33813  2sqr3minply  33865  cos9thpiminply  33873  pstmxmet  33982  esumpmono  34164  esumcvg  34171  meascnbl  34304  omsmon  34383  omsmeas  34408  dstfrvinc  34562  hgt750lemd  34733  hgt750lema  34742  hgt750leme  34743  swrdwlk  35243  derangenlem  35287  subfaclefac  35292  subfaclim  35304  erdszelem10  35316  sinccvglem  35788  iprodefisum  35857  unbdqndv2lem2  36626  itg2gt0cn  37788  ibladdnclem  37789  iblabsnc  37797  iblmulc2nc  37798  itgabsnc  37802  ftc1anclem7  37812  ftc1anclem8  37813  ftc1anc  37814  mettrifi  37870  equivbnd2  37905  heiborlem6  37929  bfplem1  37935  bfp  37937  rrnmet  37942  rrndstprj1  37943  rrndstprj2  37944  dalawlem3  40045  dalawlem4  40046  dalawlem6  40048  dalawlem9  40051  dalawlem11  40053  dalawlem12  40054  dalawlem15  40057  cdleme3c  40402  cdleme7e  40419  cdleme26e  40531  cdleme26eALTN  40533  cdleme27a  40539  cdleme32c  40615  cdleme32e  40617  cdleme32le  40619  cdlemg9b  40805  cdlemg12b  40816  cdlemg12d  40818  trlcolem  40898  trlcone  40900  cdlemk7  41020  cdlemk7u  41042  cdlemk39  41088  cdlemk11ta  41101  cdlemk11tc  41117  mapdcnvatN  41838  explt1d  42493  frlmvscadiccat  42676  3cubeslem1  42841  irrapxlem5  42983  pell1qrge1  43027  pell1qrgaplem  43030  pell14qrgapw  43033  pellqrex  43036  pellfund14  43055  jm2.17a  43117  jm2.17c  43119  acongeq  43140  jm2.19  43150  jm2.27a  43162  jm2.27c  43164  jm3.1lem2  43175  areaquad  43373  rp-isfinite6  43675  hashnzfzclim  44479  binomcxplemnotnn0  44513  absimlere  45639  monoord2xrv  45643  ltmod  45798  liminflelimsuplem  45935  dvbdfbdioolem2  46089  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  stoweidlem3  46163  stoweidlem26  46186  wallispilem1  46225  wallispilem5  46229  stirlinglem1  46234  stirlinglem5  46238  stirlinglem8  46241  stirlinglem10  46243  stirlinglem12  46245  fourierdlem6  46273  fourierdlem7  46274  fourierdlem14  46281  fourierdlem19  46286  fourierdlem35  46302  fourierdlem39  46306  fourierdlem42  46309  fourierdlem50  46316  fourierdlem73  46339  fourierdlem76  46342  fourierdlem77  46343  fourierdlem81  46347  fourierdlem90  46356  fourierdlem92  46358  fourierdlem93  46359  fourierdlem111  46377  fouriersw  46391  etransclem38  46432  sge0split  46569  ovnsslelem  46720  chnsubseq  47040  chnsuslle  47041  chnerlem1  47042  lighneallem4a  47770  rhmsubcALTV  48447  logbpw2m1  48729  dignn0flhalflem1  48777  dignn0flhalflem2  48778  1aryenef  48807  2aryenef  48818  2itscp  48943  amgmwlem  49963