Theorem 3brtr4d 5142

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111

This theorem is referenced by:  f1oiso2  7330  sucdom2OLD  9056  sucdom2  9173  ordtypelem6  9483  ttrcltr  9676  ttrclss  9680  ttrclselem2  9686  fin23lem26  10285  distrnq  10921  lediv12a  12083  recp1lt1  12088  ifle  13164  xleadd1a  13220  xlemul1a  13255  fldiv4p1lem1div2  13804  fldiv4lem1div2  13806  quoremz  13824  quoremnn0ALT  13826  intfracq  13828  modmulnn  13858  fzennn  13940  monoord2  14005  expgt1  14072  expmordi  14139  leexp2r  14146  leexp1a  14147  bernneq  14201  expmulnbnd  14207  digit1  14209  faclbnd  14262  faclbnd4lem3  14267  faclbnd4lem4  14268  faclbnd6  14271  facubnd  14272  hashdomi  14352  fzsdom2  14400  absrele  15281  absimle  15282  abstri  15304  abs2difabs  15308  limsupval2  15453  rlimrege0  15552  rlimrecl  15553  climsqz  15614  climsqz2  15615  rlimdiv  15619  rlimsqz  15623  rlimsqz2  15624  isercolllem1  15638  isercoll2  15642  fsumcvg2  15700  fsumrlim  15784  o1fsum  15786  cvgcmpce  15791  isumle  15817  climcndslem1  15822  climcndslem2  15823  harmonic  15832  expcnv  15837  explecnv  15838  geomulcvg  15849  efcllem  16050  ege2le3  16063  eflegeo  16096  rpnnen2lem4  16192  ruclem2  16207  ruclem8  16212  fsumdvds  16285  phibnd  16748  iserodd  16813  pcdvdstr  16854  pcprmpw2  16860  pockthg  16884  prmreclem4  16897  prmolefac  17024  2expltfac  17070  mod2ile  18460  odsubdvds  19508  pgpfi  19542  fislw  19562  efgredlemd  19681  efgredlem  19684  frgpcpbl  19696  rnghmsubcsetc  20549  rhmsubcsetc  20578  rhmsubcrngc  20584  rhmsubc  20605  abvres  20747  abvtrivd  20748  znrrg  21482  cstucnd  24178  psmetge0  24207  psmetres2  24209  xmetge0  24239  xmetres2  24256  imasf1oxmet  24270  comet  24408  stdbdxmet  24410  dscmet  24467  nrmmetd  24469  nmrtri  24519  tngngp  24549  nmolb2d  24613  nmoleub  24626  nmoco  24632  nmotri  24634  nmoid  24637  nmods  24639  cnmet  24666  xrsxmet  24705  metdstri  24747  metnrmlem3  24757  lebnumlem3  24869  ipcau2  25141  tcphcphlem1  25142  tcphcph  25144  trirn  25307  rrxmet  25315  rrxdstprj1  25316  minveclem2  25333  ovolunlem1a  25404  ovolscalem1  25421  volss  25441  voliunlem1  25458  volcn  25514  itg1climres  25622  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2const2  25649  itg2seq  25650  itg2mulc  25655  itg2splitlem  25656  itg2monolem1  25658  itg2i1fseqle  25662  itg2i1fseq  25663  itg2i1fseq2  25664  itg2addlem  25666  itg2cnlem1  25669  itg2cnlem2  25670  iblss  25713  itgle  25718  ibladdlem  25728  iblabs  25737  iblabsr  25738  iblmulc2  25739  itgabs  25743  bddmulibl  25747  bddiblnc  25750  dvfsumabs  25936  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsum2  25948  deg1suble  26019  deg1mul3le  26029  plyeq0lem  26122  dgrcolem2  26187  geolim3  26254  aaliou3lem2  26258  aaliou3lem8  26260  ulmdvlem1  26316  radcnvlem1  26329  radcnvlem2  26330  dvradcnv  26337  pserulm  26338  pserdvlem2  26345  abelthlem2  26349  abelthlem5  26352  abelthlem7  26355  abelth2  26359  tangtx  26421  tanabsge  26422  tanord1  26453  argregt0  26526  argrege0  26527  argimgt0  26528  abslogle  26534  logcnlem4  26561  logtayllem  26575  abscxpbnd  26670  ang180lem2  26727  atanlogsublem  26832  atans2  26848  leibpi  26859  birthdaylem3  26870  cxplim  26889  cxp2limlem  26893  cxploglim2  26896  jensenlem2  26905  jensen  26906  amgmlem  26907  emcllem2  26914  emcllem4  26916  emcllem7  26919  zetacvg  26932  lgamgulmlem2  26947  lgamgulmlem5  26950  ftalem5  26994  basellem4  27001  basellem6  27003  basellem8  27005  basellem9  27006  chtwordi  27073  chpwordi  27074  ppiwordi  27079  ppiub  27122  vmalelog  27123  chtlepsi  27124  chtleppi  27128  chtublem  27129  chtub  27130  chpub  27138  logfaclbnd  27140  logfacrlim  27142  dchrptlem3  27184  bcmono  27195  bclbnd  27198  bposlem1  27202  bposlem6  27207  bposlem9  27210  lgsqrlem4  27267  2lgslem1c  27311  chebbnd1lem1  27387  chebbnd1lem3  27389  chebbnd1  27390  chtppilimlem1  27391  vmadivsum  27400  rplogsumlem2  27403  dchrisumlema  27406  dchrisumlem3  27409  dchrmusum2  27412  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0re  27431  dchrisum0lem2a  27435  mulogsumlem  27449  mulog2sumlem1  27452  mulog2sumlem2  27453  2vmadivsumlem  27458  selberg2lem  27468  selberg3lem1  27475  selberg4lem1  27478  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntpbnd1  27504  pntlemc  27513  pntlemr  27520  pntlemk  27524  pntlemo  27525  abvcxp  27533  ostth2lem1  27536  padicabv  27548  ostth2lem2  27552  ostth2lem3  27553  ostth2lem4  27554  ostth2  27555  noextendlt  27588  noextendgt  27589  nosupbnd1  27633  nosupbnd2lem1  27634  noinfbnd1  27648  noinfbnd2lem1  27649  lltropt  27791  addsproplem2  27884  addsproplem4  27886  addsproplem5  27887  addsproplem6  27888  mulsproplem5  28030  mulsproplem6  28031  mulsproplem7  28032  mulsproplem8  28033  slemuld  28048  mulsuniflem  28059  slemul1ad  28092  precsexlem9  28124  legso  28533  trgcopy  28738  eucrct2eupth  30181  nvmtri  30607  imsmetlem  30626  vacn  30630  nmcvcn  30631  smcnlem  30633  blometi  30739  ipblnfi  30791  minvecolem2  30811  hhssnv  31200  nmcoplbi  31964  nmopcoi  32031  nmopcoadji  32037  idleop  32067  cdj1i  32369  isoun  32632  xlt2addrd  32689  nexple  32776  mgcf1o  32936  pfxchn  32942  chnub  32945  chnccats1  32948  omndmul  33035  ogrpsub  33037  gsumle  33045  cycpmconjslem2  33119  archirngz  33150  elrgspnlem1  33200  ofldchr  33299  q1pvsca  33576  lssdimle  33610  fedgmullem2  33633  fldextrspundglemul  33681  fldext2chn  33725  2sqr3minply  33777  cos9thpiminply  33785  pstmxmet  33894  esumpmono  34076  esumcvg  34083  meascnbl  34216  omsmon  34296  omsmeas  34321  dstfrvinc  34475  hgt750lemd  34646  hgt750lema  34655  hgt750leme  34656  swrdwlk  35121  derangenlem  35165  subfaclefac  35170  subfaclim  35182  erdszelem10  35194  sinccvglem  35666  iprodefisum  35735  unbdqndv2lem2  36505  itg2gt0cn  37676  ibladdnclem  37677  iblabsnc  37685  iblmulc2nc  37686  itgabsnc  37690  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  mettrifi  37758  equivbnd2  37793  heiborlem6  37817  bfplem1  37823  bfp  37825  rrnmet  37830  rrndstprj1  37831  rrndstprj2  37832  dalawlem3  39874  dalawlem4  39875  dalawlem6  39877  dalawlem9  39880  dalawlem11  39882  dalawlem12  39883  dalawlem15  39886  cdleme3c  40231  cdleme7e  40248  cdleme26e  40360  cdleme26eALTN  40362  cdleme27a  40368  cdleme32c  40444  cdleme32e  40446  cdleme32le  40448  cdlemg9b  40634  cdlemg12b  40645  cdlemg12d  40647  trlcolem  40727  trlcone  40729  cdlemk7  40849  cdlemk7u  40871  cdlemk39  40917  cdlemk11ta  40930  cdlemk11tc  40946  mapdcnvatN  41667  explt1d  42318  frlmvscadiccat  42501  3cubeslem1  42679  irrapxlem5  42821  pell1qrge1  42865  pell1qrgaplem  42868  pell14qrgapw  42871  pellqrex  42874  pellfund14  42893  jm2.17a  42956  jm2.17c  42958  acongeq  42979  jm2.19  42989  jm2.27a  43001  jm2.27c  43003  jm3.1lem2  43014  areaquad  43212  rp-isfinite6  43514  hashnzfzclim  44318  binomcxplemnotnn0  44352  absimlere  45482  monoord2xrv  45486  ltmod  45643  liminflelimsuplem  45780  dvbdfbdioolem2  45934  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem3  46008  stoweidlem26  46031  wallispilem1  46070  wallispilem5  46074  stirlinglem1  46079  stirlinglem5  46083  stirlinglem8  46086  stirlinglem10  46088  stirlinglem12  46090  fourierdlem6  46118  fourierdlem7  46119  fourierdlem14  46126  fourierdlem19  46131  fourierdlem35  46147  fourierdlem39  46151  fourierdlem42  46154  fourierdlem50  46161  fourierdlem73  46184  fourierdlem76  46187  fourierdlem77  46188  fourierdlem81  46192  fourierdlem90  46201  fourierdlem92  46203  fourierdlem93  46204  fourierdlem111  46222  fouriersw  46236  etransclem38  46277  sge0split  46414  ovnsslelem  46565  lighneallem4a  47613  rhmsubcALTV  48277  logbpw2m1  48560  dignn0flhalflem1  48608  dignn0flhalflem2  48609  1aryenef  48638  2aryenef  48649  2itscp  48774  amgmwlem  49795