Theorem 3brtr4d 5117

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086

This theorem is referenced by:  f1oiso2  7307  sucdom2  9137  ordtypelem6  9438  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  fin23lem26  10247  distrnq  10884  lediv12a  12049  recp1lt1  12054  ifle  13149  xleadd1a  13205  xlemul1a  13240  fldiv4p1lem1div2  13794  fldiv4lem1div2  13796  quoremz  13814  quoremnn0ALT  13816  intfracq  13818  modmulnn  13848  fzennn  13930  monoord2  13995  expgt1  14062  expmordi  14129  leexp2r  14136  leexp1a  14137  bernneq  14191  expmulnbnd  14197  digit1  14199  faclbnd  14252  faclbnd4lem3  14257  faclbnd4lem4  14258  faclbnd6  14261  facubnd  14262  hashdomi  14342  fzsdom2  14390  absrele  15270  absimle  15271  abstri  15293  abs2difabs  15297  limsupval2  15442  rlimrege0  15541  rlimrecl  15542  climsqz  15603  climsqz2  15604  rlimdiv  15608  rlimsqz  15612  rlimsqz2  15613  isercolllem1  15627  isercoll2  15631  fsumcvg2  15689  fsumrlim  15774  o1fsum  15776  cvgcmpce  15781  isumle  15809  climcndslem1  15814  climcndslem2  15815  harmonic  15824  expcnv  15829  explecnv  15830  geomulcvg  15841  efcllem  16042  ege2le3  16055  eflegeo  16088  rpnnen2lem4  16184  ruclem2  16199  ruclem8  16204  fsumdvds  16277  phibnd  16741  iserodd  16806  pcdvdstr  16847  pcprmpw2  16853  pockthg  16877  prmreclem4  16890  prmolefac  17017  2expltfac  17063  mod2ile  18460  pfxchn  18576  chnub  18588  chnccats1  18591  chnccat  18592  chnrev  18593  ex-chn2  18604  odsubdvds  19546  pgpfi  19580  fislw  19600  efgredlemd  19719  efgredlem  19722  frgpcpbl  19734  omndmul  20110  ogrpsub  20112  gsumle  20120  rnghmsubcsetc  20610  rhmsubcsetc  20639  rhmsubcrngc  20645  rhmsubc  20666  abvres  20808  abvtrivd  20809  znrrg  21545  ofldchr  21556  cstucnd  24248  psmetge0  24277  psmetres2  24279  xmetge0  24309  xmetres2  24326  imasf1oxmet  24340  comet  24478  stdbdxmet  24480  dscmet  24537  nrmmetd  24539  nmrtri  24589  tngngp  24619  nmolb2d  24683  nmoleub  24696  nmoco  24702  nmotri  24704  nmoid  24707  nmods  24709  cnmet  24736  xrsxmet  24775  metdstri  24817  metnrmlem3  24827  lebnumlem3  24930  ipcau2  25201  tcphcphlem1  25202  tcphcph  25204  trirn  25367  rrxmet  25375  rrxdstprj1  25376  minveclem2  25393  ovolunlem1a  25463  ovolscalem1  25480  volss  25500  voliunlem1  25517  volcn  25573  itg1climres  25681  mbfi1fseqlem5  25686  mbfi1fseqlem6  25687  itg2const2  25708  itg2seq  25709  itg2mulc  25714  itg2splitlem  25715  itg2monolem1  25717  itg2i1fseqle  25721  itg2i1fseq  25722  itg2i1fseq2  25723  itg2addlem  25725  itg2cnlem1  25728  itg2cnlem2  25729  iblss  25772  itgle  25777  ibladdlem  25787  iblabs  25796  iblabsr  25797  iblmulc2  25798  itgabs  25802  bddmulibl  25806  bddiblnc  25809  dvfsumabs  25990  dvfsumlem2  25994  dvfsum2  26001  deg1suble  26072  deg1mul3le  26082  plyeq0lem  26175  dgrcolem2  26239  geolim3  26305  aaliou3lem2  26309  aaliou3lem8  26311  ulmdvlem1  26365  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  pserulm  26387  pserdvlem2  26393  abelthlem2  26397  abelthlem5  26400  abelthlem7  26403  abelth2  26407  tangtx  26469  tanabsge  26470  tanord1  26501  argregt0  26574  argrege0  26575  argimgt0  26576  abslogle  26582  logcnlem4  26609  logtayllem  26623  abscxpbnd  26717  ang180lem2  26774  atanlogsublem  26879  atans2  26895  leibpi  26906  birthdaylem3  26917  cxplim  26935  cxp2limlem  26939  cxploglim2  26942  jensenlem2  26951  jensen  26952  amgmlem  26953  emcllem2  26960  emcllem4  26962  emcllem7  26965  zetacvg  26978  lgamgulmlem2  26993  lgamgulmlem5  26996  ftalem5  27040  basellem4  27047  basellem6  27049  basellem8  27051  basellem9  27052  chtwordi  27119  chpwordi  27120  ppiwordi  27125  ppiub  27167  vmalelog  27168  chtlepsi  27169  chtleppi  27173  chtublem  27174  chtub  27175  chpub  27183  logfaclbnd  27185  logfacrlim  27187  dchrptlem3  27229  bcmono  27240  bclbnd  27243  bposlem1  27247  bposlem6  27252  bposlem9  27255  lgsqrlem4  27312  2lgslem1c  27356  chebbnd1lem1  27432  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  vmadivsum  27445  rplogsumlem2  27448  dchrisumlema  27451  dchrisumlem3  27454  dchrmusum2  27457  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  dchrisum0flblem1  27471  dchrisum0re  27476  dchrisum0lem2a  27480  mulogsumlem  27494  mulog2sumlem1  27497  mulog2sumlem2  27498  2vmadivsumlem  27503  selberg2lem  27513  selberg3lem1  27520  selberg4lem1  27523  pntrlog2bndlem3  27542  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntpbnd1  27549  pntlemc  27558  pntlemr  27565  pntlemk  27569  pntlemo  27570  abvcxp  27578  ostth2lem1  27581  padicabv  27593  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  ostth2  27600  noextendlt  27633  noextendgt  27634  nosupbnd1  27678  nosupbnd2lem1  27679  noinfbnd1  27693  noinfbnd2lem1  27694  lltr  27854  addsproplem2  27962  addsproplem4  27964  addsproplem5  27965  addsproplem6  27966  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  lemulsd  28130  mulsuniflem  28141  lemuls1ad  28174  precsexlem9  28207  bdaypw2n0bndlem  28455  legso  28667  trgcopy  28872  eucrct2eupth  30315  nvmtri  30742  imsmetlem  30761  vacn  30765  nmcvcn  30766  smcnlem  30768  blometi  30874  ipblnfi  30926  minvecolem2  30946  hhssnv  31335  nmcoplbi  32099  nmopcoi  32166  nmopcoadji  32172  idleop  32202  cdj1i  32504  isoun  32775  xlt2addrd  32832  nexple  32917  mgcf1o  33063  cycpmconjslem2  33216  archirngz  33250  elrgspnlem1  33303  q1pvsca  33664  lssdimle  33752  fedgmullem2  33774  fldextrspundglemul  33823  extdgfialglem1  33836  fldext2chn  33872  2sqr3minply  33924  cos9thpiminply  33932  pstmxmet  34041  esumpmono  34223  esumcvg  34230  meascnbl  34363  omsmon  34442  omsmeas  34467  dstfrvinc  34621  hgt750lemd  34792  hgt750lema  34801  hgt750leme  34802  swrdwlk  35309  derangenlem  35353  subfaclefac  35358  subfaclim  35370  erdszelem10  35382  sinccvglem  35854  iprodefisum  35923  unbdqndv2lem2  36770  itg2gt0cn  37996  ibladdnclem  37997  iblabsnc  38005  iblmulc2nc  38006  itgabsnc  38010  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  mettrifi  38078  equivbnd2  38113  heiborlem6  38137  bfplem1  38143  bfp  38145  rrnmet  38150  rrndstprj1  38151  rrndstprj2  38152  dalawlem3  40319  dalawlem4  40320  dalawlem6  40322  dalawlem9  40325  dalawlem11  40327  dalawlem12  40328  dalawlem15  40331  cdleme3c  40676  cdleme7e  40693  cdleme26e  40805  cdleme26eALTN  40807  cdleme27a  40813  cdleme32c  40889  cdleme32e  40891  cdleme32le  40893  cdlemg9b  41079  cdlemg12b  41090  cdlemg12d  41092  trlcolem  41172  trlcone  41174  cdlemk7  41294  cdlemk7u  41316  cdlemk39  41362  cdlemk11ta  41375  cdlemk11tc  41391  mapdcnvatN  42112  explt1d  42755  frlmvscadiccat  42951  3cubeslem1  43116  irrapxlem5  43254  pell1qrge1  43298  pell1qrgaplem  43301  pell14qrgapw  43304  pellqrex  43307  pellfund14  43326  jm2.17a  43388  jm2.17c  43390  acongeq  43411  jm2.19  43421  jm2.27a  43433  jm2.27c  43435  jm3.1lem2  43446  areaquad  43644  rp-isfinite6  43945  hashnzfzclim  44749  binomcxplemnotnn0  44783  absimlere  45907  monoord2xrv  45911  ltmod  46066  liminflelimsuplem  46203  dvbdfbdioolem2  46357  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweidlem3  46431  stoweidlem26  46454  wallispilem1  46493  wallispilem5  46497  stirlinglem1  46502  stirlinglem5  46506  stirlinglem8  46509  stirlinglem10  46511  stirlinglem12  46513  fourierdlem6  46541  fourierdlem7  46542  fourierdlem14  46549  fourierdlem19  46554  fourierdlem35  46570  fourierdlem39  46574  fourierdlem42  46577  fourierdlem50  46584  fourierdlem73  46607  fourierdlem76  46610  fourierdlem77  46611  fourierdlem81  46615  fourierdlem90  46624  fourierdlem92  46626  fourierdlem93  46627  fourierdlem111  46645  fouriersw  46659  etransclem38  46700  sge0split  46837  ovnsslelem  46988  chnsubseq  47310  chnsuslle  47311  chnerlem1  47312  lighneallem4a  48071  rhmsubcALTV  48761  logbpw2m1  49043  dignn0flhalflem1  49091  dignn0flhalflem2  49092  1aryenef  49121  2aryenef  49132  2itscp  49257  amgmwlem  50277