Theorem 3brtr4d 5198

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

Syntax hints:   → wi 4   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  f1oiso2  7388  sucdom2OLD  9148  sucdom2  9269  ordtypelem6  9592  ttrcltr  9785  ttrclss  9789  ttrclselem2  9795  fin23lem26  10394  distrnq  11030  lediv12a  12188  recp1lt1  12193  ifle  13259  xleadd1a  13315  xlemul1a  13350  fldiv4p1lem1div2  13886  fldiv4lem1div2  13888  quoremz  13906  quoremnn0ALT  13908  intfracq  13910  modmulnn  13940  fzennn  14019  monoord2  14084  expgt1  14151  expmordi  14217  leexp2r  14224  leexp1a  14225  bernneq  14278  expmulnbnd  14284  digit1  14286  faclbnd  14339  faclbnd4lem3  14344  faclbnd4lem4  14345  faclbnd6  14348  facubnd  14349  hashdomi  14429  fzsdom2  14477  absrele  15357  absimle  15358  abstri  15379  abs2difabs  15383  limsupval2  15526  rlimrege0  15625  rlimrecl  15626  climsqz  15687  climsqz2  15688  rlimdiv  15694  rlimsqz  15698  rlimsqz2  15699  isercolllem1  15713  isercoll2  15717  fsumcvg2  15775  fsumrlim  15859  o1fsum  15861  cvgcmpce  15866  isumle  15892  climcndslem1  15897  climcndslem2  15898  harmonic  15907  expcnv  15912  explecnv  15913  geomulcvg  15924  efcllem  16125  ege2le3  16138  eflegeo  16169  rpnnen2lem4  16265  ruclem2  16280  ruclem8  16285  fsumdvds  16356  phibnd  16818  iserodd  16882  pcdvdstr  16923  pcprmpw2  16929  pockthg  16953  prmreclem4  16966  prmolefac  17093  2expltfac  17140  mod2ile  18564  odsubdvds  19613  pgpfi  19647  fislw  19667  efgredlemd  19786  efgredlem  19789  frgpcpbl  19801  rnghmsubcsetc  20655  rhmsubcsetc  20684  rhmsubcrngc  20690  rhmsubc  20711  abvres  20854  abvtrivd  20855  znrrg  21607  cstucnd  24314  psmetge0  24343  psmetres2  24345  xmetge0  24375  xmetres2  24392  imasf1oxmet  24406  comet  24547  stdbdxmet  24549  dscmet  24606  nrmmetd  24608  nmrtri  24658  tngngp  24696  nmolb2d  24760  nmoleub  24773  nmoco  24779  nmotri  24781  nmoid  24784  nmods  24786  cnmet  24813  xrsxmet  24850  metdstri  24892  metnrmlem3  24902  lebnumlem3  25014  ipcau2  25287  tcphcphlem1  25288  tcphcph  25290  trirn  25453  rrxmet  25461  rrxdstprj1  25462  minveclem2  25479  ovolunlem1a  25550  ovolscalem1  25567  volss  25587  voliunlem1  25604  volcn  25660  itg1climres  25769  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  itg2const2  25796  itg2seq  25797  itg2mulc  25802  itg2splitlem  25803  itg2monolem1  25805  itg2i1fseqle  25809  itg2i1fseq  25810  itg2i1fseq2  25811  itg2addlem  25813  itg2cnlem1  25816  itg2cnlem2  25817  iblss  25860  itgle  25865  ibladdlem  25875  iblabs  25884  iblabsr  25885  iblmulc2  25886  itgabs  25890  bddmulibl  25894  bddiblnc  25897  dvfsumabs  26083  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsum2  26095  deg1suble  26166  deg1mul3le  26176  plyeq0lem  26269  dgrcolem2  26334  geolim3  26399  aaliou3lem2  26403  aaliou3lem8  26405  ulmdvlem1  26461  radcnvlem1  26474  radcnvlem2  26475  dvradcnv  26482  pserulm  26483  pserdvlem2  26490  abelthlem2  26494  abelthlem5  26497  abelthlem7  26500  abelth2  26504  tangtx  26565  tanabsge  26566  tanord1  26597  argregt0  26670  argrege0  26671  argimgt0  26672  abslogle  26678  logcnlem4  26705  logtayllem  26719  abscxpbnd  26814  ang180lem2  26871  atanlogsublem  26976  atans2  26992  leibpi  27003  birthdaylem3  27014  cxplim  27033  cxp2limlem  27037  cxploglim2  27040  jensenlem2  27049  jensen  27050  amgmlem  27051  emcllem2  27058  emcllem4  27060  emcllem7  27063  zetacvg  27076  lgamgulmlem2  27091  lgamgulmlem5  27094  ftalem5  27138  basellem4  27145  basellem6  27147  basellem8  27149  basellem9  27150  chtwordi  27217  chpwordi  27218  ppiwordi  27223  ppiub  27266  vmalelog  27267  chtlepsi  27268  chtleppi  27272  chtublem  27273  chtub  27274  chpub  27282  logfaclbnd  27284  logfacrlim  27286  dchrptlem3  27328  bcmono  27339  bclbnd  27342  bposlem1  27346  bposlem6  27351  bposlem9  27354  lgsqrlem4  27411  2lgslem1c  27455  chebbnd1lem1  27531  chebbnd1lem3  27533  chebbnd1  27534  chtppilimlem1  27535  vmadivsum  27544  rplogsumlem2  27547  dchrisumlema  27550  dchrisumlem3  27553  dchrmusum2  27556  dchrvmasumlem3  27561  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0re  27575  dchrisum0lem2a  27579  mulogsumlem  27593  mulog2sumlem1  27596  mulog2sumlem2  27597  2vmadivsumlem  27602  selberg2lem  27612  selberg3lem1  27619  selberg4lem1  27622  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntpbnd1  27648  pntlemc  27657  pntlemr  27664  pntlemk  27668  pntlemo  27669  abvcxp  27677  ostth2lem1  27680  padicabv  27692  ostth2lem2  27696  ostth2lem3  27697  ostth2lem4  27698  ostth2  27699  noextendlt  27732  noextendgt  27733  nosupbnd1  27777  nosupbnd2lem1  27778  noinfbnd1  27792  noinfbnd2lem1  27793  lltropt  27929  addsproplem2  28021  addsproplem4  28023  addsproplem5  28024  addsproplem6  28025  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  slemuld  28182  mulsuniflem  28193  slemul1ad  28226  precsexlem9  28257  legso  28625  trgcopy  28830  eucrct2eupth  30277  nvmtri  30703  imsmetlem  30722  vacn  30726  nmcvcn  30727  smcnlem  30729  blometi  30835  ipblnfi  30887  minvecolem2  30907  hhssnv  31296  nmcoplbi  32060  nmopcoi  32127  nmopcoadji  32133  idleop  32163  cdj1i  32465  isoun  32713  xlt2addrd  32765  mgcf1o  32976  pfxchn  32982  chnub  32984  omndmul  33064  ogrpsub  33066  gsumle  33074  cycpmconjslem2  33148  archirngz  33169  ofldchr  33309  q1pvsca  33589  lssdimle  33620  fedgmullem2  33643  fldext2chn  33719  2sqr3minply  33738  pstmxmet  33843  nexple  33973  esumpmono  34043  esumcvg  34050  meascnbl  34183  omsmon  34263  omsmeas  34288  dstfrvinc  34441  hgt750lemd  34625  hgt750lema  34634  hgt750leme  34635  swrdwlk  35094  derangenlem  35139  subfaclefac  35144  subfaclim  35156  erdszelem10  35168  sinccvglem  35640  iprodefisum  35703  unbdqndv2lem2  36476  itg2gt0cn  37635  ibladdnclem  37636  iblabsnc  37644  iblmulc2nc  37645  itgabsnc  37649  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  mettrifi  37717  equivbnd2  37752  heiborlem6  37776  bfplem1  37782  bfp  37784  rrnmet  37789  rrndstprj1  37790  rrndstprj2  37791  dalawlem3  39830  dalawlem4  39831  dalawlem6  39833  dalawlem9  39836  dalawlem11  39838  dalawlem12  39839  dalawlem15  39842  cdleme3c  40187  cdleme7e  40204  cdleme26e  40316  cdleme26eALTN  40318  cdleme27a  40324  cdleme32c  40400  cdleme32e  40402  cdleme32le  40404  cdlemg9b  40590  cdlemg12b  40601  cdlemg12d  40603  trlcolem  40683  trlcone  40685  cdlemk7  40805  cdlemk7u  40827  cdlemk39  40873  cdlemk11ta  40886  cdlemk11tc  40902  mapdcnvatN  41623  factwoffsmonot  42199  explt1d  42310  frlmvscadiccat  42461  3cubeslem1  42640  irrapxlem5  42782  pell1qrge1  42826  pell1qrgaplem  42829  pell14qrgapw  42832  pellqrex  42835  pellfund14  42854  jm2.17a  42917  jm2.17c  42919  acongeq  42940  jm2.19  42950  jm2.27a  42962  jm2.27c  42964  jm3.1lem2  42975  areaquad  43177  rp-isfinite6  43480  hashnzfzclim  44291  binomcxplemnotnn0  44325  absimlere  45395  monoord2xrv  45399  ltmod  45559  dvbdfbdioolem2  45850  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweidlem3  45924  stoweidlem26  45947  wallispilem1  45986  wallispilem5  45990  stirlinglem1  45995  stirlinglem5  45999  stirlinglem8  46002  stirlinglem10  46004  stirlinglem12  46006  fourierdlem6  46034  fourierdlem7  46035  fourierdlem14  46042  fourierdlem19  46047  fourierdlem35  46063  fourierdlem39  46067  fourierdlem42  46070  fourierdlem50  46077  fourierdlem73  46100  fourierdlem76  46103  fourierdlem77  46104  fourierdlem81  46108  fourierdlem90  46117  fourierdlem92  46119  fourierdlem93  46120  fourierdlem111  46138  fouriersw  46152  etransclem38  46193  sge0split  46330  ovnsslelem  46481  lighneallem4a  47482  rhmsubcALTV  48008  logbpw2m1  48301  dignn0flhalflem1  48349  dignn0flhalflem2  48350  1aryenef  48379  2aryenef  48390  2itscp  48515  amgmwlem  48896