Theorem 3brtr4d 5106

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

Syntax hints:   → wi 4   = wceq 1539   class class class wbr 5074

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5075

This theorem is referenced by:  f1oiso2  7216  sucdom2OLD  8857  sucdom2  8977  ordtypelem6  9270  ttrcltr  9462  ttrclss  9466  ttrclselem2  9472  fin23lem26  10069  distrnq  10705  lediv12a  11856  recp1lt1  11861  ifle  12919  xleadd1a  12975  xlemul1a  13010  fldiv4p1lem1div2  13543  fldiv4lem1div2  13545  quoremz  13563  quoremnn0ALT  13565  intfracq  13567  modmulnn  13597  fzennn  13676  monoord2  13742  expgt1  13809  expmordi  13873  leexp2r  13880  leexp1a  13881  bernneq  13932  expmulnbnd  13938  digit1  13940  faclbnd  13992  faclbnd4lem3  13997  faclbnd4lem4  13998  faclbnd6  14001  facubnd  14002  hashdomi  14083  fzsdom2  14131  absrele  15008  absimle  15009  abstri  15030  abs2difabs  15034  limsupval2  15177  rlimrege0  15276  rlimrecl  15277  climsqz  15338  climsqz2  15339  rlimdiv  15345  rlimsqz  15349  rlimsqz2  15350  isercolllem1  15364  isercoll2  15368  fsumcvg2  15427  fsumrlim  15511  o1fsum  15513  cvgcmpce  15518  isumle  15544  climcndslem1  15549  climcndslem2  15550  harmonic  15559  expcnv  15564  explecnv  15565  geomulcvg  15576  efcllem  15775  ege2le3  15787  eflegeo  15818  rpnnen2lem4  15914  ruclem2  15929  ruclem8  15934  fsumdvds  16005  phibnd  16460  iserodd  16524  pcdvdstr  16565  pcprmpw2  16571  pockthg  16595  prmreclem4  16608  prmolefac  16735  2expltfac  16782  mod2ile  18200  odsubdvds  19164  pgpfi  19198  fislw  19218  efgredlemd  19338  efgredlem  19341  frgpcpbl  19353  abvres  20087  abvtrivd  20088  znrrg  20761  cstucnd  23424  psmetge0  23453  psmetres2  23455  xmetge0  23485  xmetres2  23502  imasf1oxmet  23516  comet  23657  stdbdxmet  23659  dscmet  23716  nrmmetd  23718  nmrtri  23768  tngngp  23806  nmolb2d  23870  nmoleub  23883  nmoco  23889  nmotri  23891  nmoid  23894  nmods  23896  cnmet  23923  xrsxmet  23960  metdstri  24002  metnrmlem3  24012  lebnumlem3  24114  ipcau2  24386  tcphcphlem1  24387  tcphcph  24389  trirn  24552  rrxmet  24560  rrxdstprj1  24561  minveclem2  24578  ovolunlem1a  24648  ovolscalem1  24665  volss  24685  voliunlem1  24702  volcn  24758  itg1climres  24867  mbfi1fseqlem5  24872  mbfi1fseqlem6  24873  itg2const2  24894  itg2seq  24895  itg2mulc  24900  itg2splitlem  24901  itg2monolem1  24903  itg2i1fseqle  24907  itg2i1fseq  24908  itg2i1fseq2  24909  itg2addlem  24911  itg2cnlem1  24914  itg2cnlem2  24915  iblss  24957  itgle  24962  ibladdlem  24972  iblabs  24981  iblabsr  24982  iblmulc2  24983  itgabs  24987  bddmulibl  24991  bddiblnc  24994  dvfsumabs  25175  dvfsumlem2  25179  dvfsum2  25186  deg1suble  25260  deg1mul3le  25269  plyeq0lem  25359  dgrcolem2  25423  geolim3  25487  aaliou3lem2  25491  aaliou3lem8  25493  ulmdvlem1  25547  radcnvlem1  25560  radcnvlem2  25561  dvradcnv  25568  pserulm  25569  pserdvlem2  25575  abelthlem2  25579  abelthlem5  25582  abelthlem7  25585  abelth2  25589  tangtx  25650  tanabsge  25651  tanord1  25681  argregt0  25753  argrege0  25754  argimgt0  25755  abslogle  25761  logcnlem4  25788  logtayllem  25802  abscxpbnd  25894  ang180lem2  25948  atanlogsublem  26053  atans2  26069  leibpi  26080  birthdaylem3  26091  cxplim  26109  cxp2limlem  26113  cxploglim2  26116  jensenlem2  26125  jensen  26126  amgmlem  26127  emcllem2  26134  emcllem4  26136  emcllem7  26139  zetacvg  26152  lgamgulmlem2  26167  lgamgulmlem5  26170  ftalem5  26214  basellem4  26221  basellem6  26223  basellem8  26225  basellem9  26226  chtwordi  26293  chpwordi  26294  ppiwordi  26299  ppiub  26340  vmalelog  26341  chtlepsi  26342  chtleppi  26346  chtublem  26347  chtub  26348  chpub  26356  logfaclbnd  26358  logfacrlim  26360  dchrptlem3  26402  bcmono  26413  bclbnd  26416  bposlem1  26420  bposlem6  26425  bposlem9  26428  lgsqrlem4  26485  2lgslem1c  26529  chebbnd1lem1  26605  chebbnd1lem3  26607  chebbnd1  26608  chtppilimlem1  26609  vmadivsum  26618  rplogsumlem2  26621  dchrisumlema  26624  dchrisumlem3  26627  dchrmusum2  26630  dchrvmasumlem3  26635  dchrvmasumiflem1  26637  dchrisum0flblem1  26644  dchrisum0re  26649  dchrisum0lem2a  26653  mulogsumlem  26667  mulog2sumlem1  26670  mulog2sumlem2  26671  2vmadivsumlem  26676  selberg2lem  26686  selberg3lem1  26693  selberg4lem1  26696  pntrlog2bndlem3  26715  pntrlog2bndlem5  26717  pntrlog2bndlem6  26719  pntpbnd1  26722  pntlemc  26731  pntlemr  26738  pntlemk  26742  pntlemo  26743  abvcxp  26751  ostth2lem1  26754  padicabv  26766  ostth2lem2  26770  ostth2lem3  26771  ostth2lem4  26772  ostth2  26773  legso  26948  trgcopy  27153  eucrct2eupth  28595  nvmtri  29019  imsmetlem  29038  vacn  29042  nmcvcn  29043  smcnlem  29045  blometi  29151  ipblnfi  29203  minvecolem2  29223  hhssnv  29612  nmcoplbi  30376  nmopcoi  30443  nmopcoadji  30449  idleop  30479  cdj1i  30781  isoun  31020  xlt2addrd  31067  mgcf1o  31267  omndmul  31326  ogrpsub  31328  gsumle  31336  cycpmconjslem2  31408  archirngz  31429  ofldchr  31499  lssdimle  31677  fedgmullem2  31697  pstmxmet  31833  nexple  31963  esumpmono  32033  esumcvg  32040  meascnbl  32173  omsmon  32251  omsmeas  32276  dstfrvinc  32429  hgt750lemd  32614  hgt750lema  32623  hgt750leme  32624  swrdwlk  33074  derangenlem  33119  subfaclefac  33124  subfaclim  33136  erdszelem10  33148  sinccvglem  33616  iprodefisum  33693  noextendlt  33858  noextendgt  33859  nosupbnd1  33903  nosupbnd2lem1  33904  noinfbnd1  33918  noinfbnd2lem1  33919  unbdqndv2lem2  34676  itg2gt0cn  35818  ibladdnclem  35819  iblabsnc  35827  iblmulc2nc  35828  itgabsnc  35832  ftc1anclem7  35842  ftc1anclem8  35843  ftc1anc  35844  mettrifi  35901  equivbnd2  35936  heiborlem6  35960  bfplem1  35966  bfp  35968  rrnmet  35973  rrndstprj1  35974  rrndstprj2  35975  dalawlem3  37873  dalawlem4  37874  dalawlem6  37876  dalawlem9  37879  dalawlem11  37881  dalawlem12  37882  dalawlem15  37885  cdleme3c  38230  cdleme7e  38247  cdleme26e  38359  cdleme26eALTN  38361  cdleme27a  38367  cdleme32c  38443  cdleme32e  38445  cdleme32le  38447  cdlemg9b  38633  cdlemg12b  38644  cdlemg12d  38646  trlcolem  38726  trlcone  38728  cdlemk7  38848  cdlemk7u  38870  cdlemk39  38916  cdlemk11ta  38929  cdlemk11tc  38945  mapdcnvatN  39666  factwoffsmonot  40149  frlmvscadiccat  40223  3cubeslem1  40492  irrapxlem5  40634  pell1qrge1  40678  pell1qrgaplem  40681  pell14qrgapw  40684  pellqrex  40687  pellfund14  40706  jm2.17a  40768  jm2.17c  40770  acongeq  40791  jm2.19  40801  jm2.27a  40813  jm2.27c  40815  jm3.1lem2  40826  areaquad  41033  rp-isfinite6  41093  hashnzfzclim  41899  binomcxplemnotnn0  41933  absimlere  42979  monoord2xrv  42983  ltmod  43138  dvbdfbdioolem2  43429  ioodvbdlimc1lem2  43432  ioodvbdlimc2lem  43434  stoweidlem3  43503  stoweidlem26  43526  wallispilem1  43565  wallispilem5  43569  stirlinglem1  43574  stirlinglem5  43578  stirlinglem8  43581  stirlinglem10  43583  stirlinglem12  43585  fourierdlem6  43613  fourierdlem7  43614  fourierdlem14  43621  fourierdlem19  43626  fourierdlem35  43642  fourierdlem39  43646  fourierdlem42  43649  fourierdlem50  43656  fourierdlem73  43679  fourierdlem76  43682  fourierdlem77  43683  fourierdlem81  43687  fourierdlem90  43696  fourierdlem92  43698  fourierdlem93  43699  fourierdlem111  43717  fouriersw  43731  etransclem38  43772  sge0split  43906  lighneallem4a  45016  rnghmsubcsetc  45491  rhmsubcsetc  45537  rhmsubcrngc  45543  rhmsubc  45604  rhmsubcALTV  45622  logbpw2m1  45869  dignn0flhalflem1  45917  dignn0flhalflem2  45918  1aryenef  45947  2aryenef  45958  2itscp  46083  amgmwlem  46462