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 1540   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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096

This theorem is referenced by:  f1oiso2  7293  sucdom2  9127  ordtypelem6  9434  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  fin23lem26  10238  distrnq  10874  lediv12a  12036  recp1lt1  12041  ifle  13117  xleadd1a  13173  xlemul1a  13208  fldiv4p1lem1div2  13757  fldiv4lem1div2  13759  quoremz  13777  quoremnn0ALT  13779  intfracq  13781  modmulnn  13811  fzennn  13893  monoord2  13958  expgt1  14025  expmordi  14092  leexp2r  14099  leexp1a  14100  bernneq  14154  expmulnbnd  14160  digit1  14162  faclbnd  14215  faclbnd4lem3  14220  faclbnd4lem4  14221  faclbnd6  14224  facubnd  14225  hashdomi  14305  fzsdom2  14353  absrele  15233  absimle  15234  abstri  15256  abs2difabs  15260  limsupval2  15405  rlimrege0  15504  rlimrecl  15505  climsqz  15566  climsqz2  15567  rlimdiv  15571  rlimsqz  15575  rlimsqz2  15576  isercolllem1  15590  isercoll2  15594  fsumcvg2  15652  fsumrlim  15736  o1fsum  15738  cvgcmpce  15743  isumle  15769  climcndslem1  15774  climcndslem2  15775  harmonic  15784  expcnv  15789  explecnv  15790  geomulcvg  15801  efcllem  16002  ege2le3  16015  eflegeo  16048  rpnnen2lem4  16144  ruclem2  16159  ruclem8  16164  fsumdvds  16237  phibnd  16700  iserodd  16765  pcdvdstr  16806  pcprmpw2  16812  pockthg  16836  prmreclem4  16849  prmolefac  16976  2expltfac  17022  mod2ile  18418  odsubdvds  19468  pgpfi  19502  fislw  19522  efgredlemd  19641  efgredlem  19644  frgpcpbl  19656  omndmul  20032  ogrpsub  20034  gsumle  20042  rnghmsubcsetc  20536  rhmsubcsetc  20565  rhmsubcrngc  20571  rhmsubc  20592  abvres  20734  abvtrivd  20735  znrrg  21490  ofldchr  21501  cstucnd  24187  psmetge0  24216  psmetres2  24218  xmetge0  24248  xmetres2  24265  imasf1oxmet  24279  comet  24417  stdbdxmet  24419  dscmet  24476  nrmmetd  24478  nmrtri  24528  tngngp  24558  nmolb2d  24622  nmoleub  24635  nmoco  24641  nmotri  24643  nmoid  24646  nmods  24648  cnmet  24675  xrsxmet  24714  metdstri  24756  metnrmlem3  24766  lebnumlem3  24878  ipcau2  25150  tcphcphlem1  25151  tcphcph  25153  trirn  25316  rrxmet  25324  rrxdstprj1  25325  minveclem2  25342  ovolunlem1a  25413  ovolscalem1  25430  volss  25450  voliunlem1  25467  volcn  25523  itg1climres  25631  mbfi1fseqlem5  25636  mbfi1fseqlem6  25637  itg2const2  25658  itg2seq  25659  itg2mulc  25664  itg2splitlem  25665  itg2monolem1  25667  itg2i1fseqle  25671  itg2i1fseq  25672  itg2i1fseq2  25673  itg2addlem  25675  itg2cnlem1  25678  itg2cnlem2  25679  iblss  25722  itgle  25727  ibladdlem  25737  iblabs  25746  iblabsr  25747  iblmulc2  25748  itgabs  25752  bddmulibl  25756  bddiblnc  25759  dvfsumabs  25945  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsum2  25957  deg1suble  26028  deg1mul3le  26038  plyeq0lem  26131  dgrcolem2  26196  geolim3  26263  aaliou3lem2  26267  aaliou3lem8  26269  ulmdvlem1  26325  radcnvlem1  26338  radcnvlem2  26339  dvradcnv  26346  pserulm  26347  pserdvlem2  26354  abelthlem2  26358  abelthlem5  26361  abelthlem7  26364  abelth2  26368  tangtx  26430  tanabsge  26431  tanord1  26462  argregt0  26535  argrege0  26536  argimgt0  26537  abslogle  26543  logcnlem4  26570  logtayllem  26584  abscxpbnd  26679  ang180lem2  26736  atanlogsublem  26841  atans2  26857  leibpi  26868  birthdaylem3  26879  cxplim  26898  cxp2limlem  26902  cxploglim2  26905  jensenlem2  26914  jensen  26915  amgmlem  26916  emcllem2  26923  emcllem4  26925  emcllem7  26928  zetacvg  26941  lgamgulmlem2  26956  lgamgulmlem5  26959  ftalem5  27003  basellem4  27010  basellem6  27012  basellem8  27014  basellem9  27015  chtwordi  27082  chpwordi  27083  ppiwordi  27088  ppiub  27131  vmalelog  27132  chtlepsi  27133  chtleppi  27137  chtublem  27138  chtub  27139  chpub  27147  logfaclbnd  27149  logfacrlim  27151  dchrptlem3  27193  bcmono  27204  bclbnd  27207  bposlem1  27211  bposlem6  27216  bposlem9  27219  lgsqrlem4  27276  2lgslem1c  27320  chebbnd1lem1  27396  chebbnd1lem3  27398  chebbnd1  27399  chtppilimlem1  27400  vmadivsum  27409  rplogsumlem2  27412  dchrisumlema  27415  dchrisumlem3  27418  dchrmusum2  27421  dchrvmasumlem3  27426  dchrvmasumiflem1  27428  dchrisum0flblem1  27435  dchrisum0re  27440  dchrisum0lem2a  27444  mulogsumlem  27458  mulog2sumlem1  27461  mulog2sumlem2  27462  2vmadivsumlem  27467  selberg2lem  27477  selberg3lem1  27484  selberg4lem1  27487  pntrlog2bndlem3  27506  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  pntpbnd1  27513  pntlemc  27522  pntlemr  27529  pntlemk  27533  pntlemo  27534  abvcxp  27542  ostth2lem1  27545  padicabv  27557  ostth2lem2  27561  ostth2lem3  27562  ostth2lem4  27563  ostth2  27564  noextendlt  27597  noextendgt  27598  nosupbnd1  27642  nosupbnd2lem1  27643  noinfbnd1  27657  noinfbnd2lem1  27658  lltropt  27804  addsproplem2  27900  addsproplem4  27902  addsproplem5  27903  addsproplem6  27904  mulsproplem5  28046  mulsproplem6  28047  mulsproplem7  28048  mulsproplem8  28049  slemuld  28064  mulsuniflem  28075  slemul1ad  28108  precsexlem9  28140  legso  28562  trgcopy  28767  eucrct2eupth  30207  nvmtri  30633  imsmetlem  30652  vacn  30656  nmcvcn  30657  smcnlem  30659  blometi  30765  ipblnfi  30817  minvecolem2  30837  hhssnv  31226  nmcoplbi  31990  nmopcoi  32057  nmopcoadji  32063  idleop  32093  cdj1i  32395  isoun  32658  xlt2addrd  32715  nexple  32802  mgcf1o  32958  pfxchn  32964  chnub  32967  chnccats1  32970  cycpmconjslem2  33110  archirngz  33144  elrgspnlem1  33195  q1pvsca  33548  lssdimle  33582  fedgmullem2  33605  fldextrspundglemul  33653  fldext2chn  33697  2sqr3minply  33749  cos9thpiminply  33757  pstmxmet  33866  esumpmono  34048  esumcvg  34055  meascnbl  34188  omsmon  34268  omsmeas  34293  dstfrvinc  34447  hgt750lemd  34618  hgt750lema  34627  hgt750leme  34628  swrdwlk  35102  derangenlem  35146  subfaclefac  35151  subfaclim  35163  erdszelem10  35175  sinccvglem  35647  iprodefisum  35716  unbdqndv2lem2  36486  itg2gt0cn  37657  ibladdnclem  37658  iblabsnc  37666  iblmulc2nc  37667  itgabsnc  37671  ftc1anclem7  37681  ftc1anclem8  37682  ftc1anc  37683  mettrifi  37739  equivbnd2  37774  heiborlem6  37798  bfplem1  37804  bfp  37806  rrnmet  37811  rrndstprj1  37812  rrndstprj2  37813  dalawlem3  39855  dalawlem4  39856  dalawlem6  39858  dalawlem9  39861  dalawlem11  39863  dalawlem12  39864  dalawlem15  39867  cdleme3c  40212  cdleme7e  40229  cdleme26e  40341  cdleme26eALTN  40343  cdleme27a  40349  cdleme32c  40425  cdleme32e  40427  cdleme32le  40429  cdlemg9b  40615  cdlemg12b  40626  cdlemg12d  40628  trlcolem  40708  trlcone  40710  cdlemk7  40830  cdlemk7u  40852  cdlemk39  40898  cdlemk11ta  40911  cdlemk11tc  40927  mapdcnvatN  41648  explt1d  42299  frlmvscadiccat  42482  3cubeslem1  42660  irrapxlem5  42802  pell1qrge1  42846  pell1qrgaplem  42849  pell14qrgapw  42852  pellqrex  42855  pellfund14  42874  jm2.17a  42936  jm2.17c  42938  acongeq  42959  jm2.19  42969  jm2.27a  42981  jm2.27c  42983  jm3.1lem2  42994  areaquad  43192  rp-isfinite6  43494  hashnzfzclim  44298  binomcxplemnotnn0  44332  absimlere  45462  monoord2xrv  45466  ltmod  45623  liminflelimsuplem  45760  dvbdfbdioolem2  45914  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  stoweidlem3  45988  stoweidlem26  46011  wallispilem1  46050  wallispilem5  46054  stirlinglem1  46059  stirlinglem5  46063  stirlinglem8  46066  stirlinglem10  46068  stirlinglem12  46070  fourierdlem6  46098  fourierdlem7  46099  fourierdlem14  46106  fourierdlem19  46111  fourierdlem35  46127  fourierdlem39  46131  fourierdlem42  46134  fourierdlem50  46141  fourierdlem73  46164  fourierdlem76  46167  fourierdlem77  46168  fourierdlem81  46172  fourierdlem90  46181  fourierdlem92  46183  fourierdlem93  46184  fourierdlem111  46202  fouriersw  46216  etransclem38  46257  sge0split  46394  ovnsslelem  46545  lighneallem4a  47596  rhmsubcALTV  48273  logbpw2m1  48556  dignn0flhalflem1  48604  dignn0flhalflem2  48605  1aryenef  48634  2aryenef  48645  2itscp  48770  amgmwlem  49791