Theorem breqd 5081

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 5072	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷 ↔ 𝐶𝐵𝐷))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-br 5071

This theorem is referenced by:  breq123d  5084  breqdi  5085  sbcbr123  5124  sbcbr  5125  sbcbr12g  5126  fvmptopab  7308  brfvopab  7310  mptmpoopabbrd  7894  mptmpoopabovd  7895  bropopvvv  7901  bropfvvvvlem  7902  sprmpod  8011  fprlem1  8087  wfrlem5OLD  8115  supeq123d  9139  frrlem15  9446  fpwwe2lem11  10328  fpwwe2  10330  brtrclfv  14641  dfrtrclrec2  14697  rtrclreclem3  14699  relexpindlem  14702  shftfib  14711  2shfti  14719  prdsval  17083  pwsle  17120  pwsleval  17121  imasleval  17169  issect  17382  isinv  17389  brcic  17427  ciclcl  17431  cicrcl  17432  isfunc  17495  funcres2c  17533  isfull  17542  isfth  17546  fullpropd  17552  fthpropd  17553  elhoma  17663  isposd  17956  pltval  17965  lubfval  17983  glbfval  17996  joinfval  18006  meetfval  18020  odujoin  18041  odumeet  18043  ipole  18167  eqgval  18720  unitpropd  19854  znleval  20674  ltbval  21154  opsrval  21157  lmbr  22317  metustexhalf  23618  metucn  23633  isphtpc  24063  taylthlem1  25437  ulmval  25444  tgjustf  26738  iscgrg  26777  legov  26850  ishlg  26867  opphllem5  27016  opphllem6  27017  hpgbr  27025  iscgra  27074  acopy  27098  isinag  27103  isleag  27112  iseqlg  27132  wlkonprop  27928  wksonproplem  27974  istrlson  27976  upgrwlkdvspth  28008  ispthson  28011  isspthson  28012  cyclispthon  28070  wspthsn  28114  wspthsnon  28118  iswspthsnon  28122  1pthon2v  28418  3wlkond  28436  dfconngr1  28453  isconngr  28454  isconngr1  28455  1conngr  28459  conngrv2edg  28460  minvecolem4b  29141  minvecolem4  29143  br8d  30851  ressprs  31143  resstos  31147  mntoval  31162  mgcoval  31166  mgcval  31167  isomnd  31229  submomnd  31238  ogrpaddltrd  31247  isinftm  31337  isorng  31400  rprmval  31566  metidv  31744  pstmfval  31748  faeval  32114  brfae  32116  isacycgr  33007  isacycgr1  33008  issconn  33088  satfbrsuc  33228  mclsax  33431  bj-imdirval3  35282  unceq  35681  alrmomodm  36418  relbrcoss  36491  lcvbr  36962  isopos  37121  cmtvalN  37152  isoml  37179  cvrfval  37209  cvrval  37210  pats  37226  isatl  37240  iscvlat  37264  ishlat1  37293  llnset  37446  lplnset  37470  lvolset  37513  lineset  37679  psubspset  37685  pmapfval  37697  lautset  38023  ldilfset  38049  ltrnfset  38058  trlfset  38101  diaffval  38971  dicffval  39115  dihffval  39171  prjspnvs  40380  fnwe2lem2  40792  fnwe2lem3  40793  aomclem8  40802  brfvid  41184  brfvidRP  41185  brfvrcld  41188  brfvrcld2  41189  iunrelexpuztr  41216  brtrclfv2  41224  neicvgnvor  41615  neicvgel1  41618  fperdvper  43350  upwlkbprop  45188  rngcifuestrc  45443  isprsd  46137  lubeldm2d  46140  glbeldm2d  46141  catprsc  46182  catprsc2  46183  prsthinc  46223  prstcle  46238