Theorem 3brtr4d 5062

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

Syntax hints:   → wi 4   = wceq 1538   class class class wbr 5030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031

This theorem is referenced by:  f1oiso2  7084  sucdom2  8610  ordtypelem6  8971  fin23lem26  9736  distrnq  10372  lediv12a  11522  recp1lt1  11527  ifle  12578  xleadd1a  12634  xlemul1a  12669  fldiv4p1lem1div2  13200  fldiv4lem1div2  13202  quoremz  13218  quoremnn0ALT  13220  intfracq  13222  modmulnn  13252  fzennn  13331  monoord2  13397  expgt1  13463  expmordi  13527  leexp2r  13534  leexp1a  13535  bernneq  13586  expmulnbnd  13592  digit1  13594  faclbnd  13646  faclbnd4lem3  13651  faclbnd4lem4  13652  faclbnd6  13655  facubnd  13656  hashdomi  13737  fzsdom2  13785  absrele  14660  absimle  14661  abstri  14682  abs2difabs  14686  limsupval2  14829  rlimrege0  14928  rlimrecl  14929  climsqz  14989  climsqz2  14990  rlimdiv  14994  rlimsqz  14998  rlimsqz2  14999  isercolllem1  15013  isercoll2  15017  fsumcvg2  15076  fsumrlim  15158  o1fsum  15160  cvgcmpce  15165  isumle  15191  climcndslem1  15196  climcndslem2  15197  harmonic  15206  expcnv  15211  explecnv  15212  geomulcvg  15224  efcllem  15423  ege2le3  15435  eflegeo  15466  rpnnen2lem4  15562  ruclem2  15577  ruclem8  15582  fsumdvds  15650  phibnd  16098  iserodd  16162  pcdvdstr  16202  pcprmpw2  16208  pockthg  16232  prmreclem4  16245  prmolefac  16372  2expltfac  16418  mod2ile  17708  odsubdvds  18688  pgpfi  18722  fislw  18742  efgredlemd  18862  efgredlem  18865  frgpcpbl  18877  abvres  19603  abvtrivd  19604  znrrg  20257  cstucnd  22890  psmetge0  22919  psmetres2  22921  xmetge0  22951  xmetres2  22968  imasf1oxmet  22982  comet  23120  stdbdxmet  23122  dscmet  23179  nrmmetd  23181  nmrtri  23230  tngngp  23260  nmolb2d  23324  nmoleub  23337  nmoco  23343  nmotri  23345  nmoid  23348  nmods  23350  cnmet  23377  xrsxmet  23414  metdstri  23456  metnrmlem3  23466  lebnumlem3  23568  ipcau2  23838  tcphcphlem1  23839  tcphcph  23841  trirn  24004  rrxmet  24012  rrxdstprj1  24013  minveclem2  24030  ovolunlem1a  24100  ovolscalem1  24117  volss  24137  voliunlem1  24154  volcn  24210  itg1climres  24318  mbfi1fseqlem5  24323  mbfi1fseqlem6  24324  itg2const2  24345  itg2seq  24346  itg2mulc  24351  itg2splitlem  24352  itg2monolem1  24354  itg2i1fseqle  24358  itg2i1fseq  24359  itg2i1fseq2  24360  itg2addlem  24362  itg2cnlem1  24365  itg2cnlem2  24366  iblss  24408  itgle  24413  ibladdlem  24423  iblabs  24432  iblabsr  24433  iblmulc2  24434  itgabs  24438  bddmulibl  24442  bddiblnc  24445  dvfsumabs  24626  dvfsumlem2  24630  dvfsum2  24637  deg1suble  24708  deg1mul3le  24717  plyeq0lem  24807  dgrcolem2  24871  geolim3  24935  aaliou3lem2  24939  aaliou3lem8  24941  ulmdvlem1  24995  radcnvlem1  25008  radcnvlem2  25009  dvradcnv  25016  pserulm  25017  pserdvlem2  25023  abelthlem2  25027  abelthlem5  25030  abelthlem7  25033  abelth2  25037  tangtx  25098  tanabsge  25099  tanord1  25129  argregt0  25201  argrege0  25202  argimgt0  25203  abslogle  25209  logcnlem4  25236  logtayllem  25250  abscxpbnd  25342  ang180lem2  25396  atanlogsublem  25501  atans2  25517  leibpi  25528  birthdaylem3  25539  cxplim  25557  cxp2limlem  25561  cxploglim2  25564  jensenlem2  25573  jensen  25574  amgmlem  25575  emcllem2  25582  emcllem4  25584  emcllem7  25587  zetacvg  25600  lgamgulmlem2  25615  lgamgulmlem5  25618  ftalem5  25662  basellem4  25669  basellem6  25671  basellem8  25673  basellem9  25674  chtwordi  25741  chpwordi  25742  ppiwordi  25747  ppiub  25788  vmalelog  25789  chtlepsi  25790  chtleppi  25794  chtublem  25795  chtub  25796  chpub  25804  logfaclbnd  25806  logfacrlim  25808  dchrptlem3  25850  bcmono  25861  bclbnd  25864  bposlem1  25868  bposlem6  25873  bposlem9  25876  lgsqrlem4  25933  2lgslem1c  25977  chebbnd1lem1  26053  chebbnd1lem3  26055  chebbnd1  26056  chtppilimlem1  26057  vmadivsum  26066  rplogsumlem2  26069  dchrisumlema  26072  dchrisumlem3  26075  dchrmusum2  26078  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  dchrisum0flblem1  26092  dchrisum0re  26097  dchrisum0lem2a  26101  mulogsumlem  26115  mulog2sumlem1  26118  mulog2sumlem2  26119  2vmadivsumlem  26124  selberg2lem  26134  selberg3lem1  26141  selberg4lem1  26144  pntrlog2bndlem3  26163  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntpbnd1  26170  pntlemc  26179  pntlemr  26186  pntlemk  26190  pntlemo  26191  abvcxp  26199  ostth2lem1  26202  padicabv  26214  ostth2lem2  26218  ostth2lem3  26219  ostth2lem4  26220  ostth2  26221  legso  26393  trgcopy  26598  eucrct2eupth  28030  nvmtri  28454  imsmetlem  28473  vacn  28477  nmcvcn  28478  smcnlem  28480  blometi  28586  ipblnfi  28638  minvecolem2  28658  hhssnv  29047  nmcoplbi  29811  nmopcoi  29878  nmopcoadji  29884  idleop  29914  cdj1i  30216  isoun  30461  xlt2addrd  30508  omndmul  30765  ogrpsub  30767  gsumle  30775  cycpmconjslem2  30847  archirngz  30868  ofldchr  30938  lssdimle  31094  fedgmullem2  31114  pstmxmet  31250  nexple  31378  esumpmono  31448  esumcvg  31455  meascnbl  31588  omsmon  31666  omsmeas  31691  dstfrvinc  31844  hgt750lemd  32029  hgt750lema  32038  hgt750leme  32039  swrdwlk  32486  derangenlem  32531  subfaclefac  32536  subfaclim  32548  erdszelem10  32560  sinccvglem  33028  iprodefisum  33086  noextendlt  33289  noextendgt  33290  nosupbnd1  33327  nosupbnd2lem1  33328  unbdqndv2lem2  33962  itg2gt0cn  35112  ibladdnclem  35113  iblabsnc  35121  iblmulc2nc  35122  itgabsnc  35126  ftc1anclem7  35136  ftc1anclem8  35137  ftc1anc  35138  mettrifi  35195  equivbnd2  35230  heiborlem6  35254  bfplem1  35260  bfp  35262  rrnmet  35267  rrndstprj1  35268  rrndstprj2  35269  dalawlem3  37169  dalawlem4  37170  dalawlem6  37172  dalawlem9  37175  dalawlem11  37177  dalawlem12  37178  dalawlem15  37181  cdleme3c  37526  cdleme7e  37543  cdleme26e  37655  cdleme26eALTN  37657  cdleme27a  37663  cdleme32c  37739  cdleme32e  37741  cdleme32le  37743  cdlemg9b  37929  cdlemg12b  37940  cdlemg12d  37942  trlcolem  38022  trlcone  38024  cdlemk7  38144  cdlemk7u  38166  cdlemk39  38212  cdlemk11ta  38225  cdlemk11tc  38241  mapdcnvatN  38962  factwoffsmonot  39388  frlmvscadiccat  39440  3cubeslem1  39625  irrapxlem5  39767  pell1qrge1  39811  pell1qrgaplem  39814  pell14qrgapw  39817  pellqrex  39820  pellfund14  39839  jm2.17a  39901  jm2.17c  39903  acongeq  39924  jm2.19  39934  jm2.27a  39946  jm2.27c  39948  jm3.1lem2  39959  areaquad  40166  rp-isfinite6  40226  hashnzfzclim  41026  binomcxplemnotnn0  41060  absimlere  42119  monoord2xrv  42123  ltmod  42280  dvbdfbdioolem2  42571  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  stoweidlem3  42645  stoweidlem26  42668  wallispilem1  42707  wallispilem5  42711  stirlinglem1  42716  stirlinglem5  42720  stirlinglem8  42723  stirlinglem10  42725  stirlinglem12  42727  fourierdlem6  42755  fourierdlem7  42756  fourierdlem14  42763  fourierdlem19  42768  fourierdlem35  42784  fourierdlem39  42788  fourierdlem42  42791  fourierdlem50  42798  fourierdlem73  42821  fourierdlem76  42824  fourierdlem77  42825  fourierdlem81  42829  fourierdlem90  42838  fourierdlem92  42840  fourierdlem93  42841  fourierdlem111  42859  fouriersw  42873  etransclem38  42914  sge0split  43048  lighneallem4a  44126  rnghmsubcsetc  44601  rhmsubcsetc  44647  rhmsubcrngc  44653  rhmsubc  44714  rhmsubcALTV  44732  logbpw2m1  44981  dignn0flhalflem1  45029  dignn0flhalflem2  45030  1aryenef  45059  2aryenef  45070  2itscp  45195  amgmwlem  45330