Theorem 3brtr4d 5130

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

Syntax hints:   → wi 4   = wceq 1541   class class class wbr 5098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  f1oiso2  7298  sucdom2  9127  ordtypelem6  9428  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  fin23lem26  10235  distrnq  10872  lediv12a  12035  recp1lt1  12040  ifle  13112  xleadd1a  13168  xlemul1a  13203  fldiv4p1lem1div2  13755  fldiv4lem1div2  13757  quoremz  13775  quoremnn0ALT  13777  intfracq  13779  modmulnn  13809  fzennn  13891  monoord2  13956  expgt1  14023  expmordi  14090  leexp2r  14097  leexp1a  14098  bernneq  14152  expmulnbnd  14158  digit1  14160  faclbnd  14213  faclbnd4lem3  14218  faclbnd4lem4  14219  faclbnd6  14222  facubnd  14223  hashdomi  14303  fzsdom2  14351  absrele  15231  absimle  15232  abstri  15254  abs2difabs  15258  limsupval2  15403  rlimrege0  15502  rlimrecl  15503  climsqz  15564  climsqz2  15565  rlimdiv  15569  rlimsqz  15573  rlimsqz2  15574  isercolllem1  15588  isercoll2  15592  fsumcvg2  15650  fsumrlim  15734  o1fsum  15736  cvgcmpce  15741  isumle  15767  climcndslem1  15772  climcndslem2  15773  harmonic  15782  expcnv  15787  explecnv  15788  geomulcvg  15799  efcllem  16000  ege2le3  16013  eflegeo  16046  rpnnen2lem4  16142  ruclem2  16157  ruclem8  16162  fsumdvds  16235  phibnd  16698  iserodd  16763  pcdvdstr  16804  pcprmpw2  16810  pockthg  16834  prmreclem4  16847  prmolefac  16974  2expltfac  17020  mod2ile  18417  pfxchn  18533  chnub  18545  chnccats1  18548  chnccat  18549  chnrev  18550  ex-chn2  18561  odsubdvds  19500  pgpfi  19534  fislw  19554  efgredlemd  19673  efgredlem  19676  frgpcpbl  19688  omndmul  20064  ogrpsub  20066  gsumle  20074  rnghmsubcsetc  20566  rhmsubcsetc  20595  rhmsubcrngc  20601  rhmsubc  20622  abvres  20764  abvtrivd  20765  znrrg  21520  ofldchr  21531  cstucnd  24227  psmetge0  24256  psmetres2  24258  xmetge0  24288  xmetres2  24305  imasf1oxmet  24319  comet  24457  stdbdxmet  24459  dscmet  24516  nrmmetd  24518  nmrtri  24568  tngngp  24598  nmolb2d  24662  nmoleub  24675  nmoco  24681  nmotri  24683  nmoid  24686  nmods  24688  cnmet  24715  xrsxmet  24754  metdstri  24796  metnrmlem3  24806  lebnumlem3  24918  ipcau2  25190  tcphcphlem1  25191  tcphcph  25193  trirn  25356  rrxmet  25364  rrxdstprj1  25365  minveclem2  25382  ovolunlem1a  25453  ovolscalem1  25470  volss  25490  voliunlem1  25507  volcn  25563  itg1climres  25671  mbfi1fseqlem5  25676  mbfi1fseqlem6  25677  itg2const2  25698  itg2seq  25699  itg2mulc  25704  itg2splitlem  25705  itg2monolem1  25707  itg2i1fseqle  25711  itg2i1fseq  25712  itg2i1fseq2  25713  itg2addlem  25715  itg2cnlem1  25718  itg2cnlem2  25719  iblss  25762  itgle  25767  ibladdlem  25777  iblabs  25786  iblabsr  25787  iblmulc2  25788  itgabs  25792  bddmulibl  25796  bddiblnc  25799  dvfsumabs  25985  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsum2  25997  deg1suble  26068  deg1mul3le  26078  plyeq0lem  26171  dgrcolem2  26236  geolim3  26303  aaliou3lem2  26307  aaliou3lem8  26309  ulmdvlem1  26365  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  pserulm  26387  pserdvlem2  26394  abelthlem2  26398  abelthlem5  26401  abelthlem7  26404  abelth2  26408  tangtx  26470  tanabsge  26471  tanord1  26502  argregt0  26575  argrege0  26576  argimgt0  26577  abslogle  26583  logcnlem4  26610  logtayllem  26624  abscxpbnd  26719  ang180lem2  26776  atanlogsublem  26881  atans2  26897  leibpi  26908  birthdaylem3  26919  cxplim  26938  cxp2limlem  26942  cxploglim2  26945  jensenlem2  26954  jensen  26955  amgmlem  26956  emcllem2  26963  emcllem4  26965  emcllem7  26968  zetacvg  26981  lgamgulmlem2  26996  lgamgulmlem5  26999  ftalem5  27043  basellem4  27050  basellem6  27052  basellem8  27054  basellem9  27055  chtwordi  27122  chpwordi  27123  ppiwordi  27128  ppiub  27171  vmalelog  27172  chtlepsi  27173  chtleppi  27177  chtublem  27178  chtub  27179  chpub  27187  logfaclbnd  27189  logfacrlim  27191  dchrptlem3  27233  bcmono  27244  bclbnd  27247  bposlem1  27251  bposlem6  27256  bposlem9  27259  lgsqrlem4  27316  2lgslem1c  27360  chebbnd1lem1  27436  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  vmadivsum  27449  rplogsumlem2  27452  dchrisumlema  27455  dchrisumlem3  27458  dchrmusum2  27461  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  dchrisum0flblem1  27475  dchrisum0re  27480  dchrisum0lem2a  27484  mulogsumlem  27498  mulog2sumlem1  27501  mulog2sumlem2  27502  2vmadivsumlem  27507  selberg2lem  27517  selberg3lem1  27524  selberg4lem1  27527  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntpbnd1  27553  pntlemc  27562  pntlemr  27569  pntlemk  27573  pntlemo  27574  abvcxp  27582  ostth2lem1  27585  padicabv  27597  ostth2lem2  27601  ostth2lem3  27602  ostth2lem4  27603  ostth2  27604  noextendlt  27637  noextendgt  27638  nosupbnd1  27682  nosupbnd2lem1  27683  noinfbnd1  27697  noinfbnd2lem1  27698  lltr  27858  addsproplem2  27966  addsproplem4  27968  addsproplem5  27969  addsproplem6  27970  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  lemulsd  28134  mulsuniflem  28145  lemuls1ad  28178  precsexlem9  28211  bdaypw2n0bndlem  28459  legso  28671  trgcopy  28876  eucrct2eupth  30320  nvmtri  30746  imsmetlem  30765  vacn  30769  nmcvcn  30770  smcnlem  30772  blometi  30878  ipblnfi  30930  minvecolem2  30950  hhssnv  31339  nmcoplbi  32103  nmopcoi  32170  nmopcoadji  32176  idleop  32206  cdj1i  32508  isoun  32781  xlt2addrd  32839  nexple  32925  mgcf1o  33085  cycpmconjslem2  33237  archirngz  33271  elrgspnlem1  33324  q1pvsca  33685  lssdimle  33764  fedgmullem2  33787  fldextrspundglemul  33836  extdgfialglem1  33849  fldext2chn  33885  2sqr3minply  33937  cos9thpiminply  33945  pstmxmet  34054  esumpmono  34236  esumcvg  34243  meascnbl  34376  omsmon  34455  omsmeas  34480  dstfrvinc  34634  hgt750lemd  34805  hgt750lema  34814  hgt750leme  34815  swrdwlk  35321  derangenlem  35365  subfaclefac  35370  subfaclim  35382  erdszelem10  35394  sinccvglem  35866  iprodefisum  35935  unbdqndv2lem2  36710  itg2gt0cn  37876  ibladdnclem  37877  iblabsnc  37885  iblmulc2nc  37886  itgabsnc  37890  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  mettrifi  37958  equivbnd2  37993  heiborlem6  38017  bfplem1  38023  bfp  38025  rrnmet  38030  rrndstprj1  38031  rrndstprj2  38032  dalawlem3  40133  dalawlem4  40134  dalawlem6  40136  dalawlem9  40139  dalawlem11  40141  dalawlem12  40142  dalawlem15  40145  cdleme3c  40490  cdleme7e  40507  cdleme26e  40619  cdleme26eALTN  40621  cdleme27a  40627  cdleme32c  40703  cdleme32e  40705  cdleme32le  40707  cdlemg9b  40893  cdlemg12b  40904  cdlemg12d  40906  trlcolem  40986  trlcone  40988  cdlemk7  41108  cdlemk7u  41130  cdlemk39  41176  cdlemk11ta  41189  cdlemk11tc  41205  mapdcnvatN  41926  explt1d  42578  frlmvscadiccat  42761  3cubeslem1  42926  irrapxlem5  43068  pell1qrge1  43112  pell1qrgaplem  43115  pell14qrgapw  43118  pellqrex  43121  pellfund14  43140  jm2.17a  43202  jm2.17c  43204  acongeq  43225  jm2.19  43235  jm2.27a  43247  jm2.27c  43249  jm3.1lem2  43260  areaquad  43458  rp-isfinite6  43759  hashnzfzclim  44563  binomcxplemnotnn0  44597  absimlere  45723  monoord2xrv  45727  ltmod  45882  liminflelimsuplem  46019  dvbdfbdioolem2  46173  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  stoweidlem3  46247  stoweidlem26  46270  wallispilem1  46309  wallispilem5  46313  stirlinglem1  46318  stirlinglem5  46322  stirlinglem8  46325  stirlinglem10  46327  stirlinglem12  46329  fourierdlem6  46357  fourierdlem7  46358  fourierdlem14  46365  fourierdlem19  46370  fourierdlem35  46386  fourierdlem39  46390  fourierdlem42  46393  fourierdlem50  46400  fourierdlem73  46423  fourierdlem76  46426  fourierdlem77  46427  fourierdlem81  46431  fourierdlem90  46440  fourierdlem92  46442  fourierdlem93  46443  fourierdlem111  46461  fouriersw  46475  etransclem38  46516  sge0split  46653  ovnsslelem  46804  chnsubseq  47124  chnsuslle  47125  chnerlem1  47126  lighneallem4a  47854  rhmsubcALTV  48531  logbpw2m1  48813  dignn0flhalflem1  48861  dignn0flhalflem2  48862  1aryenef  48891  2aryenef  48902  2itscp  49027  amgmwlem  50047