Theorem 3brtr4d 5118

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

Syntax hints:   → wi 4   = wceq 1542   class class class wbr 5086

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  f1oiso2  7300  sucdom2  9130  ordtypelem6  9431  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  fin23lem26  10238  distrnq  10875  lediv12a  12040  recp1lt1  12045  ifle  13140  xleadd1a  13196  xlemul1a  13231  fldiv4p1lem1div2  13785  fldiv4lem1div2  13787  quoremz  13805  quoremnn0ALT  13807  intfracq  13809  modmulnn  13839  fzennn  13921  monoord2  13986  expgt1  14053  expmordi  14120  leexp2r  14127  leexp1a  14128  bernneq  14182  expmulnbnd  14188  digit1  14190  faclbnd  14243  faclbnd4lem3  14248  faclbnd4lem4  14249  faclbnd6  14252  facubnd  14253  hashdomi  14333  fzsdom2  14381  absrele  15261  absimle  15262  abstri  15284  abs2difabs  15288  limsupval2  15433  rlimrege0  15532  rlimrecl  15533  climsqz  15594  climsqz2  15595  rlimdiv  15599  rlimsqz  15603  rlimsqz2  15604  isercolllem1  15618  isercoll2  15622  fsumcvg2  15680  fsumrlim  15765  o1fsum  15767  cvgcmpce  15772  isumle  15800  climcndslem1  15805  climcndslem2  15806  harmonic  15815  expcnv  15820  explecnv  15821  geomulcvg  15832  efcllem  16033  ege2le3  16046  eflegeo  16079  rpnnen2lem4  16175  ruclem2  16190  ruclem8  16195  fsumdvds  16268  phibnd  16732  iserodd  16797  pcdvdstr  16838  pcprmpw2  16844  pockthg  16868  prmreclem4  16881  prmolefac  17008  2expltfac  17054  mod2ile  18451  pfxchn  18567  chnub  18579  chnccats1  18582  chnccat  18583  chnrev  18584  ex-chn2  18595  odsubdvds  19537  pgpfi  19571  fislw  19591  efgredlemd  19710  efgredlem  19713  frgpcpbl  19725  omndmul  20101  ogrpsub  20103  gsumle  20111  rnghmsubcsetc  20601  rhmsubcsetc  20630  rhmsubcrngc  20636  rhmsubc  20657  abvres  20799  abvtrivd  20800  znrrg  21555  ofldchr  21566  cstucnd  24258  psmetge0  24287  psmetres2  24289  xmetge0  24319  xmetres2  24336  imasf1oxmet  24350  comet  24488  stdbdxmet  24490  dscmet  24547  nrmmetd  24549  nmrtri  24599  tngngp  24629  nmolb2d  24693  nmoleub  24706  nmoco  24712  nmotri  24714  nmoid  24717  nmods  24719  cnmet  24746  xrsxmet  24785  metdstri  24827  metnrmlem3  24837  lebnumlem3  24940  ipcau2  25211  tcphcphlem1  25212  tcphcph  25214  trirn  25377  rrxmet  25385  rrxdstprj1  25386  minveclem2  25403  ovolunlem1a  25473  ovolscalem1  25490  volss  25510  voliunlem1  25527  volcn  25583  itg1climres  25691  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  itg2const2  25718  itg2seq  25719  itg2mulc  25724  itg2splitlem  25725  itg2monolem1  25727  itg2i1fseqle  25731  itg2i1fseq  25732  itg2i1fseq2  25733  itg2addlem  25735  itg2cnlem1  25738  itg2cnlem2  25739  iblss  25782  itgle  25787  ibladdlem  25797  iblabs  25806  iblabsr  25807  iblmulc2  25808  itgabs  25812  bddmulibl  25816  bddiblnc  25819  dvfsumabs  26000  dvfsumlem2  26004  dvfsum2  26011  deg1suble  26082  deg1mul3le  26092  plyeq0lem  26185  dgrcolem2  26249  geolim3  26316  aaliou3lem2  26320  aaliou3lem8  26322  ulmdvlem1  26378  radcnvlem1  26391  radcnvlem2  26392  dvradcnv  26399  pserulm  26400  pserdvlem2  26406  abelthlem2  26410  abelthlem5  26413  abelthlem7  26416  abelth2  26420  tangtx  26482  tanabsge  26483  tanord1  26514  argregt0  26587  argrege0  26588  argimgt0  26589  abslogle  26595  logcnlem4  26622  logtayllem  26636  abscxpbnd  26730  ang180lem2  26787  atanlogsublem  26892  atans2  26908  leibpi  26919  birthdaylem3  26930  cxplim  26949  cxp2limlem  26953  cxploglim2  26956  jensenlem2  26965  jensen  26966  amgmlem  26967  emcllem2  26974  emcllem4  26976  emcllem7  26979  zetacvg  26992  lgamgulmlem2  27007  lgamgulmlem5  27010  ftalem5  27054  basellem4  27061  basellem6  27063  basellem8  27065  basellem9  27066  chtwordi  27133  chpwordi  27134  ppiwordi  27139  ppiub  27181  vmalelog  27182  chtlepsi  27183  chtleppi  27187  chtublem  27188  chtub  27189  chpub  27197  logfaclbnd  27199  logfacrlim  27201  dchrptlem3  27243  bcmono  27254  bclbnd  27257  bposlem1  27261  bposlem6  27266  bposlem9  27269  lgsqrlem4  27326  2lgslem1c  27370  chebbnd1lem1  27446  chebbnd1lem3  27448  chebbnd1  27449  chtppilimlem1  27450  vmadivsum  27459  rplogsumlem2  27462  dchrisumlema  27465  dchrisumlem3  27468  dchrmusum2  27471  dchrvmasumlem3  27476  dchrvmasumiflem1  27478  dchrisum0flblem1  27485  dchrisum0re  27490  dchrisum0lem2a  27494  mulogsumlem  27508  mulog2sumlem1  27511  mulog2sumlem2  27512  2vmadivsumlem  27517  selberg2lem  27527  selberg3lem1  27534  selberg4lem1  27537  pntrlog2bndlem3  27556  pntrlog2bndlem5  27558  pntrlog2bndlem6  27560  pntpbnd1  27563  pntlemc  27572  pntlemr  27579  pntlemk  27583  pntlemo  27584  abvcxp  27592  ostth2lem1  27595  padicabv  27607  ostth2lem2  27611  ostth2lem3  27612  ostth2lem4  27613  ostth2  27614  noextendlt  27647  noextendgt  27648  nosupbnd1  27692  nosupbnd2lem1  27693  noinfbnd1  27707  noinfbnd2lem1  27708  lltr  27868  addsproplem2  27976  addsproplem4  27978  addsproplem5  27979  addsproplem6  27980  mulsproplem5  28126  mulsproplem6  28127  mulsproplem7  28128  mulsproplem8  28129  lemulsd  28144  mulsuniflem  28155  lemuls1ad  28188  precsexlem9  28221  bdaypw2n0bndlem  28469  legso  28681  trgcopy  28886  eucrct2eupth  30330  nvmtri  30757  imsmetlem  30776  vacn  30780  nmcvcn  30781  smcnlem  30783  blometi  30889  ipblnfi  30941  minvecolem2  30961  hhssnv  31350  nmcoplbi  32114  nmopcoi  32181  nmopcoadji  32187  idleop  32217  cdj1i  32519  isoun  32790  xlt2addrd  32847  nexple  32932  mgcf1o  33078  cycpmconjslem2  33231  archirngz  33265  elrgspnlem1  33318  q1pvsca  33679  lssdimle  33767  fedgmullem2  33790  fldextrspundglemul  33839  extdgfialglem1  33852  fldext2chn  33888  2sqr3minply  33940  cos9thpiminply  33948  pstmxmet  34057  esumpmono  34239  esumcvg  34246  meascnbl  34379  omsmon  34458  omsmeas  34483  dstfrvinc  34637  hgt750lemd  34808  hgt750lema  34817  hgt750leme  34818  swrdwlk  35325  derangenlem  35369  subfaclefac  35374  subfaclim  35386  erdszelem10  35398  sinccvglem  35870  iprodefisum  35939  unbdqndv2lem2  36786  itg2gt0cn  38010  ibladdnclem  38011  iblabsnc  38019  iblmulc2nc  38020  itgabsnc  38024  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  mettrifi  38092  equivbnd2  38127  heiborlem6  38151  bfplem1  38157  bfp  38159  rrnmet  38164  rrndstprj1  38165  rrndstprj2  38166  dalawlem3  40333  dalawlem4  40334  dalawlem6  40336  dalawlem9  40339  dalawlem11  40341  dalawlem12  40342  dalawlem15  40345  cdleme3c  40690  cdleme7e  40707  cdleme26e  40819  cdleme26eALTN  40821  cdleme27a  40827  cdleme32c  40903  cdleme32e  40905  cdleme32le  40907  cdlemg9b  41093  cdlemg12b  41104  cdlemg12d  41106  trlcolem  41186  trlcone  41188  cdlemk7  41308  cdlemk7u  41330  cdlemk39  41376  cdlemk11ta  41389  cdlemk11tc  41405  mapdcnvatN  42126  explt1d  42769  frlmvscadiccat  42965  3cubeslem1  43130  irrapxlem5  43272  pell1qrge1  43316  pell1qrgaplem  43319  pell14qrgapw  43322  pellqrex  43325  pellfund14  43344  jm2.17a  43406  jm2.17c  43408  acongeq  43429  jm2.19  43439  jm2.27a  43451  jm2.27c  43453  jm3.1lem2  43464  areaquad  43662  rp-isfinite6  43963  hashnzfzclim  44767  binomcxplemnotnn0  44801  absimlere  45925  monoord2xrv  45929  ltmod  46084  liminflelimsuplem  46221  dvbdfbdioolem2  46375  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  stoweidlem3  46449  stoweidlem26  46472  wallispilem1  46511  wallispilem5  46515  stirlinglem1  46520  stirlinglem5  46524  stirlinglem8  46527  stirlinglem10  46529  stirlinglem12  46531  fourierdlem6  46559  fourierdlem7  46560  fourierdlem14  46567  fourierdlem19  46572  fourierdlem35  46588  fourierdlem39  46592  fourierdlem42  46595  fourierdlem50  46602  fourierdlem73  46625  fourierdlem76  46628  fourierdlem77  46629  fourierdlem81  46633  fourierdlem90  46642  fourierdlem92  46644  fourierdlem93  46645  fourierdlem111  46663  fouriersw  46677  etransclem38  46718  sge0split  46855  ovnsslelem  47006  chnsubseq  47326  chnsuslle  47327  chnerlem1  47328  lighneallem4a  48083  rhmsubcALTV  48773  logbpw2m1  49055  dignn0flhalflem1  49103  dignn0flhalflem2  49104  1aryenef  49133  2aryenef  49144  2itscp  49269  amgmwlem  50289