Theorem 3brtr4d 5179

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

Syntax hints:   → wi 4   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148

This theorem is referenced by:  f1oiso2  7371  sucdom2OLD  9120  sucdom2  9240  ordtypelem6  9560  ttrcltr  9753  ttrclss  9757  ttrclselem2  9763  fin23lem26  10362  distrnq  10998  lediv12a  12158  recp1lt1  12163  ifle  13235  xleadd1a  13291  xlemul1a  13326  fldiv4p1lem1div2  13871  fldiv4lem1div2  13873  quoremz  13891  quoremnn0ALT  13893  intfracq  13895  modmulnn  13925  fzennn  14005  monoord2  14070  expgt1  14137  expmordi  14203  leexp2r  14210  leexp1a  14211  bernneq  14264  expmulnbnd  14270  digit1  14272  faclbnd  14325  faclbnd4lem3  14330  faclbnd4lem4  14331  faclbnd6  14334  facubnd  14335  hashdomi  14415  fzsdom2  14463  absrele  15343  absimle  15344  abstri  15365  abs2difabs  15369  limsupval2  15512  rlimrege0  15611  rlimrecl  15612  climsqz  15673  climsqz2  15674  rlimdiv  15678  rlimsqz  15682  rlimsqz2  15683  isercolllem1  15697  isercoll2  15701  fsumcvg2  15759  fsumrlim  15843  o1fsum  15845  cvgcmpce  15850  isumle  15876  climcndslem1  15881  climcndslem2  15882  harmonic  15891  expcnv  15896  explecnv  15897  geomulcvg  15908  efcllem  16109  ege2le3  16122  eflegeo  16153  rpnnen2lem4  16249  ruclem2  16264  ruclem8  16269  fsumdvds  16341  phibnd  16804  iserodd  16868  pcdvdstr  16909  pcprmpw2  16915  pockthg  16939  prmreclem4  16952  prmolefac  17079  2expltfac  17126  mod2ile  18551  odsubdvds  19603  pgpfi  19637  fislw  19657  efgredlemd  19776  efgredlem  19779  frgpcpbl  19791  rnghmsubcsetc  20649  rhmsubcsetc  20678  rhmsubcrngc  20684  rhmsubc  20705  abvres  20848  abvtrivd  20849  znrrg  21601  cstucnd  24308  psmetge0  24337  psmetres2  24339  xmetge0  24369  xmetres2  24386  imasf1oxmet  24400  comet  24541  stdbdxmet  24543  dscmet  24600  nrmmetd  24602  nmrtri  24652  tngngp  24690  nmolb2d  24754  nmoleub  24767  nmoco  24773  nmotri  24775  nmoid  24778  nmods  24780  cnmet  24807  xrsxmet  24844  metdstri  24886  metnrmlem3  24896  lebnumlem3  25008  ipcau2  25281  tcphcphlem1  25282  tcphcph  25284  trirn  25447  rrxmet  25455  rrxdstprj1  25456  minveclem2  25473  ovolunlem1a  25544  ovolscalem1  25561  volss  25581  voliunlem1  25598  volcn  25654  itg1climres  25763  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2const2  25790  itg2seq  25791  itg2mulc  25796  itg2splitlem  25797  itg2monolem1  25799  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  itg2cnlem1  25810  itg2cnlem2  25811  iblss  25854  itgle  25859  ibladdlem  25869  iblabs  25878  iblabsr  25879  iblmulc2  25880  itgabs  25884  bddmulibl  25888  bddiblnc  25891  dvfsumabs  26077  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsum2  26089  deg1suble  26160  deg1mul3le  26170  plyeq0lem  26263  dgrcolem2  26328  geolim3  26395  aaliou3lem2  26399  aaliou3lem8  26401  ulmdvlem1  26457  radcnvlem1  26470  radcnvlem2  26471  dvradcnv  26478  pserulm  26479  pserdvlem2  26486  abelthlem2  26490  abelthlem5  26493  abelthlem7  26496  abelth2  26500  tangtx  26561  tanabsge  26562  tanord1  26593  argregt0  26666  argrege0  26667  argimgt0  26668  abslogle  26674  logcnlem4  26701  logtayllem  26715  abscxpbnd  26810  ang180lem2  26867  atanlogsublem  26972  atans2  26988  leibpi  26999  birthdaylem3  27010  cxplim  27029  cxp2limlem  27033  cxploglim2  27036  jensenlem2  27045  jensen  27046  amgmlem  27047  emcllem2  27054  emcllem4  27056  emcllem7  27059  zetacvg  27072  lgamgulmlem2  27087  lgamgulmlem5  27090  ftalem5  27134  basellem4  27141  basellem6  27143  basellem8  27145  basellem9  27146  chtwordi  27213  chpwordi  27214  ppiwordi  27219  ppiub  27262  vmalelog  27263  chtlepsi  27264  chtleppi  27268  chtublem  27269  chtub  27270  chpub  27278  logfaclbnd  27280  logfacrlim  27282  dchrptlem3  27324  bcmono  27335  bclbnd  27338  bposlem1  27342  bposlem6  27347  bposlem9  27350  lgsqrlem4  27407  2lgslem1c  27451  chebbnd1lem1  27527  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  vmadivsum  27540  rplogsumlem2  27543  dchrisumlema  27546  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0re  27571  dchrisum0lem2a  27575  mulogsumlem  27589  mulog2sumlem1  27592  mulog2sumlem2  27593  2vmadivsumlem  27598  selberg2lem  27608  selberg3lem1  27615  selberg4lem1  27618  pntrlog2bndlem3  27637  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntpbnd1  27644  pntlemc  27653  pntlemr  27660  pntlemk  27664  pntlemo  27665  abvcxp  27673  ostth2lem1  27676  padicabv  27688  ostth2lem2  27692  ostth2lem3  27693  ostth2lem4  27694  ostth2  27695  noextendlt  27728  noextendgt  27729  nosupbnd1  27773  nosupbnd2lem1  27774  noinfbnd1  27788  noinfbnd2lem1  27789  lltropt  27925  addsproplem2  28017  addsproplem4  28019  addsproplem5  28020  addsproplem6  28021  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  slemuld  28178  mulsuniflem  28189  slemul1ad  28222  precsexlem9  28253  legso  28621  trgcopy  28826  eucrct2eupth  30273  nvmtri  30699  imsmetlem  30718  vacn  30722  nmcvcn  30723  smcnlem  30725  blometi  30831  ipblnfi  30883  minvecolem2  30903  hhssnv  31292  nmcoplbi  32056  nmopcoi  32123  nmopcoadji  32129  idleop  32159  cdj1i  32461  isoun  32716  xlt2addrd  32768  mgcf1o  32977  pfxchn  32983  chnub  32985  omndmul  33073  ogrpsub  33075  gsumle  33083  cycpmconjslem2  33157  archirngz  33178  elrgspnlem1  33231  ofldchr  33323  q1pvsca  33603  lssdimle  33634  fedgmullem2  33657  fldext2chn  33733  2sqr3minply  33752  pstmxmet  33857  nexple  33989  esumpmono  34059  esumcvg  34066  meascnbl  34199  omsmon  34279  omsmeas  34304  dstfrvinc  34457  hgt750lemd  34641  hgt750lema  34650  hgt750leme  34651  swrdwlk  35110  derangenlem  35155  subfaclefac  35160  subfaclim  35172  erdszelem10  35184  sinccvglem  35656  iprodefisum  35720  unbdqndv2lem2  36492  itg2gt0cn  37661  ibladdnclem  37662  iblabsnc  37670  iblmulc2nc  37671  itgabsnc  37675  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  mettrifi  37743  equivbnd2  37778  heiborlem6  37802  bfplem1  37808  bfp  37810  rrnmet  37815  rrndstprj1  37816  rrndstprj2  37817  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  factwoffsmonot  42223  explt1d  42336  frlmvscadiccat  42492  3cubeslem1  42671  irrapxlem5  42813  pell1qrge1  42857  pell1qrgaplem  42860  pell14qrgapw  42863  pellqrex  42866  pellfund14  42885  jm2.17a  42948  jm2.17c  42950  acongeq  42971  jm2.19  42981  jm2.27a  42993  jm2.27c  42995  jm3.1lem2  43006  areaquad  43204  rp-isfinite6  43507  hashnzfzclim  44317  binomcxplemnotnn0  44351  absimlere  45429  monoord2xrv  45433  ltmod  45593  dvbdfbdioolem2  45884  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweidlem3  45958  stoweidlem26  45981  wallispilem1  46020  wallispilem5  46024  stirlinglem1  46029  stirlinglem5  46033  stirlinglem8  46036  stirlinglem10  46038  stirlinglem12  46040  fourierdlem6  46068  fourierdlem7  46069  fourierdlem14  46076  fourierdlem19  46081  fourierdlem35  46097  fourierdlem39  46101  fourierdlem42  46104  fourierdlem50  46111  fourierdlem73  46134  fourierdlem76  46137  fourierdlem77  46138  fourierdlem81  46142  fourierdlem90  46151  fourierdlem92  46153  fourierdlem93  46154  fourierdlem111  46172  fouriersw  46186  etransclem38  46227  sge0split  46364  ovnsslelem  46515  lighneallem4a  47532  rhmsubcALTV  48128  logbpw2m1  48416  dignn0flhalflem1  48464  dignn0flhalflem2  48465  1aryenef  48494  2aryenef  48505  2itscp  48630  amgmwlem  49032