Theorem 3brtr4d 5181

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

Syntax hints:   → wi 4   = wceq 1533   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150

This theorem is referenced by:  f1oiso2  7359  sucdom2OLD  9107  sucdom2  9231  ordtypelem6  9548  ttrcltr  9741  ttrclss  9745  ttrclselem2  9751  fin23lem26  10350  distrnq  10986  lediv12a  12140  recp1lt1  12145  ifle  13211  xleadd1a  13267  xlemul1a  13302  fldiv4p1lem1div2  13836  fldiv4lem1div2  13838  quoremz  13856  quoremnn0ALT  13858  intfracq  13860  modmulnn  13890  fzennn  13969  monoord2  14034  expgt1  14101  expmordi  14167  leexp2r  14174  leexp1a  14175  bernneq  14227  expmulnbnd  14233  digit1  14235  faclbnd  14285  faclbnd4lem3  14290  faclbnd4lem4  14291  faclbnd6  14294  facubnd  14295  hashdomi  14375  fzsdom2  14423  absrele  15291  absimle  15292  abstri  15313  abs2difabs  15317  limsupval2  15460  rlimrege0  15559  rlimrecl  15560  climsqz  15621  climsqz2  15622  rlimdiv  15628  rlimsqz  15632  rlimsqz2  15633  isercolllem1  15647  isercoll2  15651  fsumcvg2  15709  fsumrlim  15793  o1fsum  15795  cvgcmpce  15800  isumle  15826  climcndslem1  15831  climcndslem2  15832  harmonic  15841  expcnv  15846  explecnv  15847  geomulcvg  15858  efcllem  16057  ege2le3  16070  eflegeo  16101  rpnnen2lem4  16197  ruclem2  16212  ruclem8  16217  fsumdvds  16288  phibnd  16743  iserodd  16807  pcdvdstr  16848  pcprmpw2  16854  pockthg  16878  prmreclem4  16891  prmolefac  17018  2expltfac  17065  mod2ile  18489  odsubdvds  19538  pgpfi  19572  fislw  19592  efgredlemd  19711  efgredlem  19714  frgpcpbl  19726  rnghmsubcsetc  20578  rhmsubcsetc  20607  rhmsubcrngc  20613  rhmsubc  20634  abvres  20731  abvtrivd  20732  znrrg  21516  cstucnd  24233  psmetge0  24262  psmetres2  24264  xmetge0  24294  xmetres2  24311  imasf1oxmet  24325  comet  24466  stdbdxmet  24468  dscmet  24525  nrmmetd  24527  nmrtri  24577  tngngp  24615  nmolb2d  24679  nmoleub  24692  nmoco  24698  nmotri  24700  nmoid  24703  nmods  24705  cnmet  24732  xrsxmet  24769  metdstri  24811  metnrmlem3  24821  lebnumlem3  24933  ipcau2  25206  tcphcphlem1  25207  tcphcph  25209  trirn  25372  rrxmet  25380  rrxdstprj1  25381  minveclem2  25398  ovolunlem1a  25469  ovolscalem1  25486  volss  25506  voliunlem1  25523  volcn  25579  itg1climres  25688  mbfi1fseqlem5  25693  mbfi1fseqlem6  25694  itg2const2  25715  itg2seq  25716  itg2mulc  25721  itg2splitlem  25722  itg2monolem1  25724  itg2i1fseqle  25728  itg2i1fseq  25729  itg2i1fseq2  25730  itg2addlem  25732  itg2cnlem1  25735  itg2cnlem2  25736  iblss  25778  itgle  25783  ibladdlem  25793  iblabs  25802  iblabsr  25803  iblmulc2  25804  itgabs  25808  bddmulibl  25812  bddiblnc  25815  dvfsumabs  26001  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsum2  26013  deg1suble  26087  deg1mul3le  26097  plyeq0lem  26189  dgrcolem2  26254  geolim3  26319  aaliou3lem2  26323  aaliou3lem8  26325  ulmdvlem1  26381  radcnvlem1  26394  radcnvlem2  26395  dvradcnv  26402  pserulm  26403  pserdvlem2  26410  abelthlem2  26414  abelthlem5  26417  abelthlem7  26420  abelth2  26424  tangtx  26485  tanabsge  26486  tanord1  26516  argregt0  26589  argrege0  26590  argimgt0  26591  abslogle  26597  logcnlem4  26624  logtayllem  26638  abscxpbnd  26733  ang180lem2  26787  atanlogsublem  26892  atans2  26908  leibpi  26919  birthdaylem3  26930  cxplim  26949  cxp2limlem  26953  cxploglim2  26956  jensenlem2  26965  jensen  26966  amgmlem  26967  emcllem2  26974  emcllem4  26976  emcllem7  26979  zetacvg  26992  lgamgulmlem2  27007  lgamgulmlem5  27010  ftalem5  27054  basellem4  27061  basellem6  27063  basellem8  27065  basellem9  27066  chtwordi  27133  chpwordi  27134  ppiwordi  27139  ppiub  27182  vmalelog  27183  chtlepsi  27184  chtleppi  27188  chtublem  27189  chtub  27190  chpub  27198  logfaclbnd  27200  logfacrlim  27202  dchrptlem3  27244  bcmono  27255  bclbnd  27258  bposlem1  27262  bposlem6  27267  bposlem9  27270  lgsqrlem4  27327  2lgslem1c  27371  chebbnd1lem1  27447  chebbnd1lem3  27449  chebbnd1  27450  chtppilimlem1  27451  vmadivsum  27460  rplogsumlem2  27463  dchrisumlema  27466  dchrisumlem3  27469  dchrmusum2  27472  dchrvmasumlem3  27477  dchrvmasumiflem1  27479  dchrisum0flblem1  27486  dchrisum0re  27491  dchrisum0lem2a  27495  mulogsumlem  27509  mulog2sumlem1  27512  mulog2sumlem2  27513  2vmadivsumlem  27518  selberg2lem  27528  selberg3lem1  27535  selberg4lem1  27538  pntrlog2bndlem3  27557  pntrlog2bndlem5  27559  pntrlog2bndlem6  27561  pntpbnd1  27564  pntlemc  27573  pntlemr  27580  pntlemk  27584  pntlemo  27585  abvcxp  27593  ostth2lem1  27596  padicabv  27608  ostth2lem2  27612  ostth2lem3  27613  ostth2lem4  27614  ostth2  27615  noextendlt  27648  noextendgt  27649  nosupbnd1  27693  nosupbnd2lem1  27694  noinfbnd1  27708  noinfbnd2lem1  27709  lltropt  27845  addsproplem2  27933  addsproplem4  27935  addsproplem5  27936  addsproplem6  27937  mulsproplem5  28070  mulsproplem6  28071  mulsproplem7  28072  mulsproplem8  28073  slemuld  28088  mulsuniflem  28099  slemul1ad  28132  precsexlem9  28163  legso  28475  trgcopy  28680  eucrct2eupth  30127  nvmtri  30553  imsmetlem  30572  vacn  30576  nmcvcn  30577  smcnlem  30579  blometi  30685  ipblnfi  30737  minvecolem2  30757  hhssnv  31146  nmcoplbi  31910  nmopcoi  31977  nmopcoadji  31983  idleop  32013  cdj1i  32315  isoun  32563  xlt2addrd  32610  mgcf1o  32819  omndmul  32884  ogrpsub  32886  gsumle  32894  cycpmconjslem2  32968  archirngz  32989  ofldchr  33128  q1pvsca  33402  lssdimle  33433  fedgmullem2  33456  pstmxmet  33626  nexple  33756  esumpmono  33826  esumcvg  33833  meascnbl  33966  omsmon  34046  omsmeas  34071  dstfrvinc  34224  hgt750lemd  34408  hgt750lema  34417  hgt750leme  34418  swrdwlk  34864  derangenlem  34909  subfaclefac  34914  subfaclim  34926  erdszelem10  34938  sinccvglem  35404  iprodefisum  35463  unbdqndv2lem2  36113  itg2gt0cn  37276  ibladdnclem  37277  iblabsnc  37285  iblmulc2nc  37286  itgabsnc  37290  ftc1anclem7  37300  ftc1anclem8  37301  ftc1anc  37302  mettrifi  37358  equivbnd2  37393  heiborlem6  37417  bfplem1  37423  bfp  37425  rrnmet  37430  rrndstprj1  37431  rrndstprj2  37432  dalawlem3  39473  dalawlem4  39474  dalawlem6  39476  dalawlem9  39479  dalawlem11  39481  dalawlem12  39482  dalawlem15  39485  cdleme3c  39830  cdleme7e  39847  cdleme26e  39959  cdleme26eALTN  39961  cdleme27a  39967  cdleme32c  40043  cdleme32e  40045  cdleme32le  40047  cdlemg9b  40233  cdlemg12b  40244  cdlemg12d  40246  trlcolem  40326  trlcone  40328  cdlemk7  40448  cdlemk7u  40470  cdlemk39  40516  cdlemk11ta  40529  cdlemk11tc  40545  mapdcnvatN  41266  factwoffsmonot  41825  frlmvscadiccat  41881  3cubeslem1  42243  irrapxlem5  42385  pell1qrge1  42429  pell1qrgaplem  42432  pell14qrgapw  42435  pellqrex  42438  pellfund14  42457  jm2.17a  42520  jm2.17c  42522  acongeq  42543  jm2.19  42553  jm2.27a  42565  jm2.27c  42567  jm3.1lem2  42578  areaquad  42783  rp-isfinite6  43087  hashnzfzclim  43898  binomcxplemnotnn0  43932  absimlere  44997  monoord2xrv  45001  ltmod  45161  dvbdfbdioolem2  45452  ioodvbdlimc1lem2  45455  ioodvbdlimc2lem  45457  stoweidlem3  45526  stoweidlem26  45549  wallispilem1  45588  wallispilem5  45592  stirlinglem1  45597  stirlinglem5  45601  stirlinglem8  45604  stirlinglem10  45606  stirlinglem12  45608  fourierdlem6  45636  fourierdlem7  45637  fourierdlem14  45644  fourierdlem19  45649  fourierdlem35  45665  fourierdlem39  45669  fourierdlem42  45672  fourierdlem50  45679  fourierdlem73  45702  fourierdlem76  45705  fourierdlem77  45706  fourierdlem81  45710  fourierdlem90  45719  fourierdlem92  45721  fourierdlem93  45722  fourierdlem111  45740  fouriersw  45754  etransclem38  45795  sge0split  45932  ovnsslelem  46083  lighneallem4a  47082  rhmsubcALTV  47530  logbpw2m1  47823  dignn0flhalflem1  47871  dignn0flhalflem2  47872  1aryenef  47901  2aryenef  47912  2itscp  48037  amgmwlem  48418