Theorem 3brtr4d 5129

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

Syntax hints:   → wi 4   = wceq 1559   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  f1oiso2  7331  sucdom2  9165  ordtypelem6  9465  ttrcltr  9665  ttrclss  9669  ttrclselem2  9675  fin23lem26  10276  distrnq  10913  lediv12a  12079  recp1lt1  12084  ifle  13194  xleadd1a  13250  xlemul1a  13285  fldiv4p1lem1div2  13839  fldiv4lem1div2  13841  quoremz  13859  quoremnn0ALT  13861  intfracq  13863  modmulnn  13893  fzennn  13975  monoord2  14040  expgt1  14107  expmordi  14174  leexp2r  14181  leexp1a  14182  bernneq  14236  expmulnbnd  14242  digit1  14244  faclbnd  14297  faclbnd4lem3  14302  faclbnd4lem4  14303  faclbnd6  14306  facubnd  14307  hashdomi  14387  fzsdom2  14435  absrele  15326  absimle  15327  abstri  15349  abs2difabs  15353  limsupval2  15498  rlimrege0  15597  rlimrecl  15598  climsqz  15659  climsqz2  15660  rlimdiv  15664  rlimsqz  15668  rlimsqz2  15669  isercolllem1  15683  isercoll2  15687  fsumcvg2  15745  fsumrlim  15830  o1fsum  15832  cvgcmpce  15837  isumle  15865  climcndslem1  15870  climcndslem2  15871  harmonic  15880  expcnv  15885  explecnv  15886  geomulcvg  15897  efcllem  16098  ege2le3  16111  eflegeo  16144  rpnnen2lem4  16240  ruclem2  16255  ruclem8  16260  fsumdvds  16333  phibnd  16797  iserodd  16862  pcdvdstr  16903  pcprmpw2  16909  pockthg  16933  prmreclem4  16946  prmolefac  17073  2expltfac  17119  mod2ile  18517  pfxchn  18633  chnub  18645  chnccats1  18648  chnccat  18649  chnrev  18650  ex-chn2  18661  odsubdvds  19602  pgpfi  19636  fislw  19656  efgredlemd  19775  efgredlem  19778  frgpcpbl  19790  omndmul  20166  ogrpsub  20168  gsumle  20176  rnghmsubcsetc  20670  rhmsubcsetc  20699  rhmsubcrngc  20705  rhmsubc  20726  abvres  20868  abvtrivd  20869  znrrg  21605  ofldchr  21616  cstucnd  24331  psmetge0  24360  psmetres2  24362  xmetge0  24392  xmetres2  24409  imasf1oxmet  24423  comet  24561  stdbdxmet  24563  dscmet  24620  nrmmetd  24622  nmrtri  24672  tngngp  24702  nmolb2d  24766  nmoleub  24779  nmoco  24785  nmotri  24787  nmoid  24790  nmods  24792  cnmet  24819  xrsxmet  24858  metdstri  24900  metnrmlem3  24910  lebnumlem3  25013  ipcau2  25284  tcphcphlem1  25285  tcphcph  25287  trirn  25450  rrxmet  25458  rrxdstprj1  25459  minveclem2  25476  ovolunlem1a  25546  ovolscalem1  25563  volss  25583  voliunlem1  25600  volcn  25656  itg1climres  25764  mbfi1fseqlem5  25769  mbfi1fseqlem6  25770  itg2const2  25791  itg2seq  25792  itg2mulc  25797  itg2splitlem  25798  itg2monolem1  25800  itg2i1fseqle  25804  itg2i1fseq  25805  itg2i1fseq2  25806  itg2addlem  25808  itg2cnlem1  25811  itg2cnlem2  25812  iblss  25855  itgle  25860  ibladdlem  25870  iblabs  25879  iblabsr  25880  iblmulc2  25881  itgabs  25885  bddmulibl  25889  bddiblnc  25892  dvfsumabs  26073  dvfsumlem2  26077  dvfsum2  26084  deg1suble  26155  deg1mul3le  26165  plyeq0lem  26258  dgrcolem2  26322  geolim3  26391  aaliou3lem2  26395  aaliou3lem8  26397  ulmdvlem1  26451  radcnvlem1  26464  radcnvlem2  26465  dvradcnv  26472  pserulm  26473  pserdvlem2  26479  abelthlem2  26483  abelthlem5  26486  abelthlem7  26489  abelth2  26493  tangtx  26558  tanabsge  26559  tanord1  26590  argregt0  26663  argrege0  26664  argimgt0  26665  abslogle  26671  logcnlem4  26698  logtayllem  26712  abscxpbnd  26806  ang180lem2  26863  atanlogsublem  26968  atans2  26984  leibpi  26995  birthdaylem3  27006  cxplim  27024  cxp2limlem  27028  cxploglim2  27031  jensenlem2  27040  jensen  27041  amgmlem  27042  emcllem2  27049  emcllem4  27051  emcllem7  27054  zetacvg  27067  lgamgulmlem2  27082  lgamgulmlem5  27085  ftalem5  27129  basellem4  27136  basellem6  27138  basellem8  27140  basellem9  27141  chtwordi  27208  chpwordi  27209  ppiwordi  27214  ppiub  27256  vmalelog  27257  chtlepsi  27258  chtleppi  27262  chtublem  27263  chtub  27264  chpub  27272  logfaclbnd  27274  logfacrlim  27276  dchrptlem3  27318  bcmono  27329  bclbnd  27332  bposlem1  27336  bposlem6  27341  bposlem9  27344  lgsqrlem4  27401  2lgslem1c  27445  chebbnd1lem1  27521  chebbnd1lem3  27523  chebbnd1  27524  chtppilimlem1  27525  vmadivsum  27534  rplogsumlem2  27537  dchrisumlema  27540  dchrisumlem3  27543  dchrmusum2  27546  dchrvmasumlem3  27551  dchrvmasumiflem1  27553  dchrisum0flblem1  27560  dchrisum0re  27565  dchrisum0lem2a  27569  mulogsumlem  27583  mulog2sumlem1  27586  mulog2sumlem2  27587  2vmadivsumlem  27592  selberg2lem  27602  selberg3lem1  27609  selberg4lem1  27612  pntrlog2bndlem3  27631  pntrlog2bndlem5  27633  pntrlog2bndlem6  27635  pntpbnd1  27638  pntlemc  27647  pntlemr  27654  pntlemk  27658  pntlemo  27659  abvcxp  27667  ostth2lem1  27670  padicabv  27682  ostth2lem2  27686  ostth2lem3  27687  ostth2lem4  27688  ostth2  27689  noextendlt  27721  noextendgt  27722  nosupbnd1  27766  nosupbnd2lem1  27767  noinfbnd1  27781  noinfbnd2lem1  27782  lltr  27943  addsproplem2  28051  addsproplem4  28053  addsproplem5  28054  addsproplem6  28055  mulsproplem5  28201  mulsproplem6  28202  mulsproplem7  28203  mulsproplem8  28204  lemulsd  28219  mulsuniflem  28230  lemuls1ad  28263  precsexlem9  28296  bdaypw2n0bndlem  28544  legso  28756  trgcopy  28961  eucrct2eupth  30404  nvmtri  30831  imsmetlem  30850  vacn  30854  nmcvcn  30855  smcnlem  30857  blometi  30963  ipblnfi  31015  minvecolem2  31035  hhssnv  31424  nmcoplbi  32188  nmopcoi  32255  nmopcoadji  32261  idleop  32291  cdj1i  32593  isoun  32865  xlt2addrd  32922  nexple  32996  mgcf1o  33142  cycpmconjslem2  33296  archirngz  33330  elrgspnlem1  33384  q1pvsca  33761  lssdimle  33866  fedgmullem2  33888  fldextrspundglemul  33937  extdgfialglem1  33950  fldext2chn  33986  2sqr3minply  34038  cos9thpiminply  34046  pstmxmet  34155  esumpmono  34337  esumcvg  34344  meascnbl  34477  omsmon  34556  omsmeas  34581  dstfrvinc  34735  hgt750lemd  34903  hgt750lema  34912  hgt750leme  34913  swrdwlk  35438  derangenlem  35482  subfaclefac  35487  subfaclim  35499  erdszelem10  35511  sinccvglem  35983  iprodefisum  36052  unbdqndv2lem2  36909  itg2gt0cn  38135  ibladdnclem  38136  iblabsnc  38144  iblmulc2nc  38145  itgabsnc  38149  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  mettrifi  38217  equivbnd2  38252  heiborlem6  38276  bfplem1  38282  bfp  38284  rrnmet  38289  rrndstprj1  38290  rrndstprj2  38291  dalawlem3  40458  dalawlem4  40459  dalawlem6  40461  dalawlem9  40464  dalawlem11  40466  dalawlem12  40467  dalawlem15  40470  cdleme3c  40815  cdleme7e  40832  cdleme26e  40944  cdleme26eALTN  40946  cdleme27a  40952  cdleme32c  41028  cdleme32e  41030  cdleme32le  41032  cdlemg9b  41218  cdlemg12b  41229  cdlemg12d  41231  trlcolem  41311  trlcone  41313  cdlemk7  41433  cdlemk7u  41455  cdlemk39  41501  cdlemk11ta  41514  cdlemk11tc  41530  mapdcnvatN  42251  explt1d  42893  frlmvscadiccat  43089  3cubeslem1  43226  irrapxlem5  43364  pell1qrge1  43408  pell1qrgaplem  43411  pell14qrgapw  43414  pellqrex  43417  pellfund14  43436  jm2.17a  43498  jm2.17c  43500  acongeq  43521  jm2.19  43531  jm2.27a  43543  jm2.27c  43545  jm3.1lem2  43556  areaquad  43754  rp-isfinite6  44055  hashnzfzclim  44859  binomcxplemnotnn0  44893  absimlere  46014  monoord2xrv  46018  ltmod  46173  liminflelimsuplem  46310  dvbdfbdioolem2  46464  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  stoweidlem3  46538  stoweidlem26  46561  wallispilem1  46600  wallispilem5  46604  stirlinglem1  46609  stirlinglem5  46613  stirlinglem8  46616  stirlinglem10  46618  stirlinglem12  46620  fourierdlem6  46648  fourierdlem7  46649  fourierdlem14  46656  fourierdlem19  46661  fourierdlem35  46677  fourierdlem39  46681  fourierdlem42  46684  fourierdlem50  46691  fourierdlem73  46714  fourierdlem76  46717  fourierdlem77  46718  fourierdlem81  46722  fourierdlem90  46731  fourierdlem92  46733  fourierdlem93  46734  fourierdlem111  46752  fouriersw  46766  etransclem38  46807  sge0split  46944  ovnsslelem  47095  chnsubseq  47417  chnsuslle  47418  chnerlem1  47419  lighneallem4a  48178  rhmsubcALTV  48868  logbpw2m1  49150  dignn0flhalflem1  49198  dignn0flhalflem2  49199  1aryenef  49228  2aryenef  49239  2itscp  49364  amgmwlem  50384