Theorem breqd 5097

Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)

Hypothesis

Ref	Expression
breq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
breqd	⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

Proof of Theorem breqd

Step	Hyp	Ref	Expression
1		breq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		breq 5088	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

Syntax hints:   → wi 4   ↔ wb 206   = 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-ex 1782  df-cleq 2729  df-clel 2812  df-br 5087

This theorem is referenced by:  breq123d  5100  breqdi  5101  sbcbr123  5140  sbcbr  5141  sbcbr12g  5142  fvmptopab  7413  brfvopab  7415  mptmpoopabbrd  8024  mptmpoopabovd  8025  bropopvvv  8031  bropfvvvvlem  8032  sprmpod  8165  fprlem1  8241  supeq123d  9354  frrlem15  9670  fpwwe2lem11  10553  fpwwe2  10555  brtrclfv  14926  dfrtrclrec2  14982  rtrclreclem3  14984  relexpindlem  14987  shftfib  14996  2shfti  15004  prdsval  17376  pwsle  17414  pwsleval  17415  imasleval  17463  issect  17678  isinv  17685  brcic  17723  ciclcl  17727  cicrcl  17728  isfunc  17789  funcres2c  17828  isfull  17837  isfth  17841  fullpropd  17847  fthpropd  17848  elhoma  17957  isposd  18246  pltval  18254  lubfval  18272  glbfval  18285  joinfval  18295  meetfval  18309  odujoin  18330  odumeet  18332  resstos  18354  ipole  18458  eqgval  19110  isomnd  20056  submomnd  20065  ogrpaddltrd  20073  unitpropd  20355  rngcifuestrc  20574  isorng  20796  znleval  21511  ltbval  21999  opsrval  22002  lmbr  23201  metustexhalf  24499  metucn  24514  isphtpc  24939  taylthlem1  26321  ulmval  26329  tgjustf  28529  iscgrg  28568  legov  28641  ishlg  28658  opphllem5  28807  opphllem6  28808  hpgbr  28816  iscgra  28865  acopy  28889  isinag  28894  isleag  28903  iseqlg  28923  wlkonprop  29714  wksonproplem  29760  istrlson  29762  upgrwlkdvspth  29796  ispthson  29799  isspthson  29800  cyclispthon  29861  wspthsn  29905  wspthsnon  29909  iswspthsnon  29913  1pthon2v  30212  3wlkond  30230  dfconngr1  30247  isconngr  30248  isconngr1  30249  1conngr  30253  conngrv2edg  30254  minvecolem4b  30938  minvecolem4  30940  br8d  32670  ressprs  33031  mntoval  33047  mgcoval  33051  mgcval  33052  isinftm  33247  rprmval  33581  metidv  34042  pstmfval  34046  faeval  34396  brfae  34398  isacycgr  35333  isacycgr1  35334  issconn  35414  satfbrsuc  35554  mclsax  35757  weiunpo  36653  weiunfr  36655  bj-imdirval3  37496  unceq  37909  alrmomodm  38671  relbrcoss  38848  lcvbr  39458  isopos  39617  cmtvalN  39648  isoml  39675  cvrfval  39705  cvrval  39706  pats  39722  isatl  39736  iscvlat  39760  ishlat1  39789  llnset  39942  lplnset  39966  lvolset  40009  lineset  40175  psubspset  40181  pmapfval  40193  lautset  40519  ldilfset  40545  ltrnfset  40554  trlfset  40597  diaffval  41467  dicffval  41611  dihffval  41667  prjspnvs  43052  fnwe2lem2  43482  fnwe2lem3  43483  aomclem8  43492  brfvid  44117  brfvidRP  44118  brfvrcld  44121  brfvrcld2  44122  iunrelexpuztr  44149  brtrclfv2  44157  neicvgnvor  44546  neicvgel1  44549  fperdvper  46351  upwlkbprop  48572  isprsd  49388  lubeldm2d  49391  glbeldm2d  49392  catprsc  49446  catprsc2  49447  oppccicb  49484  funcoppc2  49576  uptpos  49631  prsthinc  49897  prstcle  49989  lanup  50074  ranup  50075  islmd  50098  cmddu  50101  lmdran  50104  cmdlan  50105