Theorem 3brtr4d 5151

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

Syntax hints:   → wi 4   = wceq 1540   class class class wbr 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120

This theorem is referenced by:  f1oiso2  7344  sucdom2OLD  9094  sucdom2  9215  ordtypelem6  9535  ttrcltr  9728  ttrclss  9732  ttrclselem2  9738  fin23lem26  10337  distrnq  10973  lediv12a  12133  recp1lt1  12138  ifle  13211  xleadd1a  13267  xlemul1a  13302  fldiv4p1lem1div2  13850  fldiv4lem1div2  13852  quoremz  13870  quoremnn0ALT  13872  intfracq  13874  modmulnn  13904  fzennn  13984  monoord2  14049  expgt1  14116  expmordi  14183  leexp2r  14190  leexp1a  14191  bernneq  14245  expmulnbnd  14251  digit1  14253  faclbnd  14306  faclbnd4lem3  14311  faclbnd4lem4  14312  faclbnd6  14315  facubnd  14316  hashdomi  14396  fzsdom2  14444  absrele  15325  absimle  15326  abstri  15347  abs2difabs  15351  limsupval2  15494  rlimrege0  15593  rlimrecl  15594  climsqz  15655  climsqz2  15656  rlimdiv  15660  rlimsqz  15664  rlimsqz2  15665  isercolllem1  15679  isercoll2  15683  fsumcvg2  15741  fsumrlim  15825  o1fsum  15827  cvgcmpce  15832  isumle  15858  climcndslem1  15863  climcndslem2  15864  harmonic  15873  expcnv  15878  explecnv  15879  geomulcvg  15890  efcllem  16091  ege2le3  16104  eflegeo  16137  rpnnen2lem4  16233  ruclem2  16248  ruclem8  16253  fsumdvds  16325  phibnd  16788  iserodd  16853  pcdvdstr  16894  pcprmpw2  16900  pockthg  16924  prmreclem4  16937  prmolefac  17064  2expltfac  17110  mod2ile  18502  odsubdvds  19550  pgpfi  19584  fislw  19604  efgredlemd  19723  efgredlem  19726  frgpcpbl  19738  rnghmsubcsetc  20591  rhmsubcsetc  20620  rhmsubcrngc  20626  rhmsubc  20647  abvres  20789  abvtrivd  20790  znrrg  21524  cstucnd  24220  psmetge0  24249  psmetres2  24251  xmetge0  24281  xmetres2  24298  imasf1oxmet  24312  comet  24450  stdbdxmet  24452  dscmet  24509  nrmmetd  24511  nmrtri  24561  tngngp  24591  nmolb2d  24655  nmoleub  24668  nmoco  24674  nmotri  24676  nmoid  24679  nmods  24681  cnmet  24708  xrsxmet  24747  metdstri  24789  metnrmlem3  24799  lebnumlem3  24911  ipcau2  25184  tcphcphlem1  25185  tcphcph  25187  trirn  25350  rrxmet  25358  rrxdstprj1  25359  minveclem2  25376  ovolunlem1a  25447  ovolscalem1  25464  volss  25484  voliunlem1  25501  volcn  25557  itg1climres  25665  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  itg2const2  25692  itg2seq  25693  itg2mulc  25698  itg2splitlem  25699  itg2monolem1  25701  itg2i1fseqle  25705  itg2i1fseq  25706  itg2i1fseq2  25707  itg2addlem  25709  itg2cnlem1  25712  itg2cnlem2  25713  iblss  25756  itgle  25761  ibladdlem  25771  iblabs  25780  iblabsr  25781  iblmulc2  25782  itgabs  25786  bddmulibl  25790  bddiblnc  25793  dvfsumabs  25979  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsum2  25991  deg1suble  26062  deg1mul3le  26072  plyeq0lem  26165  dgrcolem2  26230  geolim3  26297  aaliou3lem2  26301  aaliou3lem8  26303  ulmdvlem1  26359  radcnvlem1  26372  radcnvlem2  26373  dvradcnv  26380  pserulm  26381  pserdvlem2  26388  abelthlem2  26392  abelthlem5  26395  abelthlem7  26398  abelth2  26402  tangtx  26464  tanabsge  26465  tanord1  26496  argregt0  26569  argrege0  26570  argimgt0  26571  abslogle  26577  logcnlem4  26604  logtayllem  26618  abscxpbnd  26713  ang180lem2  26770  atanlogsublem  26875  atans2  26891  leibpi  26902  birthdaylem3  26913  cxplim  26932  cxp2limlem  26936  cxploglim2  26939  jensenlem2  26948  jensen  26949  amgmlem  26950  emcllem2  26957  emcllem4  26959  emcllem7  26962  zetacvg  26975  lgamgulmlem2  26990  lgamgulmlem5  26993  ftalem5  27037  basellem4  27044  basellem6  27046  basellem8  27048  basellem9  27049  chtwordi  27116  chpwordi  27117  ppiwordi  27122  ppiub  27165  vmalelog  27166  chtlepsi  27167  chtleppi  27171  chtublem  27172  chtub  27173  chpub  27181  logfaclbnd  27183  logfacrlim  27185  dchrptlem3  27227  bcmono  27238  bclbnd  27241  bposlem1  27245  bposlem6  27250  bposlem9  27253  lgsqrlem4  27310  2lgslem1c  27354  chebbnd1lem1  27430  chebbnd1lem3  27432  chebbnd1  27433  chtppilimlem1  27434  vmadivsum  27443  rplogsumlem2  27446  dchrisumlema  27449  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  dchrisum0re  27474  dchrisum0lem2a  27478  mulogsumlem  27492  mulog2sumlem1  27495  mulog2sumlem2  27496  2vmadivsumlem  27501  selberg2lem  27511  selberg3lem1  27518  selberg4lem1  27521  pntrlog2bndlem3  27540  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntpbnd1  27547  pntlemc  27556  pntlemr  27563  pntlemk  27567  pntlemo  27568  abvcxp  27576  ostth2lem1  27579  padicabv  27591  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  ostth2  27598  noextendlt  27631  noextendgt  27632  nosupbnd1  27676  nosupbnd2lem1  27677  noinfbnd1  27691  noinfbnd2lem1  27692  lltropt  27828  addsproplem2  27920  addsproplem4  27922  addsproplem5  27923  addsproplem6  27924  mulsproplem5  28063  mulsproplem6  28064  mulsproplem7  28065  mulsproplem8  28066  slemuld  28081  mulsuniflem  28092  slemul1ad  28125  precsexlem9  28156  legso  28524  trgcopy  28729  eucrct2eupth  30172  nvmtri  30598  imsmetlem  30617  vacn  30621  nmcvcn  30622  smcnlem  30624  blometi  30730  ipblnfi  30782  minvecolem2  30802  hhssnv  31191  nmcoplbi  31955  nmopcoi  32022  nmopcoadji  32028  idleop  32058  cdj1i  32360  isoun  32625  xlt2addrd  32682  nexple  32769  mgcf1o  32929  pfxchn  32935  chnub  32938  chnccats1  32941  omndmul  33028  ogrpsub  33030  gsumle  33038  cycpmconjslem2  33112  archirngz  33133  elrgspnlem1  33183  ofldchr  33282  q1pvsca  33559  lssdimle  33593  fedgmullem2  33616  fldextrspundglemul  33666  fldext2chn  33708  2sqr3minply  33760  cos9thpiminply  33768  pstmxmet  33874  esumpmono  34056  esumcvg  34063  meascnbl  34196  omsmon  34276  omsmeas  34301  dstfrvinc  34455  hgt750lemd  34626  hgt750lema  34635  hgt750leme  34636  swrdwlk  35095  derangenlem  35139  subfaclefac  35144  subfaclim  35156  erdszelem10  35168  sinccvglem  35640  iprodefisum  35704  unbdqndv2lem2  36474  itg2gt0cn  37645  ibladdnclem  37646  iblabsnc  37654  iblmulc2nc  37655  itgabsnc  37659  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  mettrifi  37727  equivbnd2  37762  heiborlem6  37786  bfplem1  37792  bfp  37794  rrnmet  37799  rrndstprj1  37800  rrndstprj2  37801  dalawlem3  39838  dalawlem4  39839  dalawlem6  39841  dalawlem9  39844  dalawlem11  39846  dalawlem12  39847  dalawlem15  39850  cdleme3c  40195  cdleme7e  40212  cdleme26e  40324  cdleme26eALTN  40326  cdleme27a  40332  cdleme32c  40408  cdleme32e  40410  cdleme32le  40412  cdlemg9b  40598  cdlemg12b  40609  cdlemg12d  40611  trlcolem  40691  trlcone  40693  cdlemk7  40813  cdlemk7u  40835  cdlemk39  40881  cdlemk11ta  40894  cdlemk11tc  40910  mapdcnvatN  41631  factwoffsmonot  42201  explt1d  42319  frlmvscadiccat  42476  3cubeslem1  42654  irrapxlem5  42796  pell1qrge1  42840  pell1qrgaplem  42843  pell14qrgapw  42846  pellqrex  42849  pellfund14  42868  jm2.17a  42931  jm2.17c  42933  acongeq  42954  jm2.19  42964  jm2.27a  42976  jm2.27c  42978  jm3.1lem2  42989  areaquad  43187  rp-isfinite6  43489  hashnzfzclim  44294  binomcxplemnotnn0  44328  absimlere  45454  monoord2xrv  45458  ltmod  45615  liminflelimsuplem  45752  dvbdfbdioolem2  45906  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  stoweidlem3  45980  stoweidlem26  46003  wallispilem1  46042  wallispilem5  46046  stirlinglem1  46051  stirlinglem5  46055  stirlinglem8  46058  stirlinglem10  46060  stirlinglem12  46062  fourierdlem6  46090  fourierdlem7  46091  fourierdlem14  46098  fourierdlem19  46103  fourierdlem35  46119  fourierdlem39  46123  fourierdlem42  46126  fourierdlem50  46133  fourierdlem73  46156  fourierdlem76  46159  fourierdlem77  46160  fourierdlem81  46164  fourierdlem90  46173  fourierdlem92  46175  fourierdlem93  46176  fourierdlem111  46194  fouriersw  46208  etransclem38  46249  sge0split  46386  ovnsslelem  46537  lighneallem4a  47570  rhmsubcALTV  48208  logbpw2m1  48495  dignn0flhalflem1  48543  dignn0flhalflem2  48544  1aryenef  48573  2aryenef  48584  2itscp  48709  amgmwlem  49614