Theorem breqd 5086

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-br 5076

This theorem is referenced by:  breq123d  5089  breqdi  5090  sbcbr123  5129  sbcbr  5130  sbcbr12g  5131  fvmptopab  7338  fvmptopabOLD  7339  brfvopab  7341  mptmpoopabbrd  7930  mptmpoopabovd  7931  mptmpoopabbrdOLD  7932  mptmpoopabovdOLD  7933  bropopvvv  7939  bropfvvvvlem  7940  sprmpod  8049  fprlem1  8125  wfrlem5OLD  8153  supeq123d  9218  frrlem15  9524  fpwwe2lem11  10406  fpwwe2  10408  brtrclfv  14722  dfrtrclrec2  14778  rtrclreclem3  14780  relexpindlem  14783  shftfib  14792  2shfti  14800  prdsval  17175  pwsle  17212  pwsleval  17213  imasleval  17261  issect  17474  isinv  17481  brcic  17519  ciclcl  17523  cicrcl  17524  isfunc  17588  funcres2c  17626  isfull  17635  isfth  17639  fullpropd  17645  fthpropd  17646  elhoma  17756  isposd  18050  pltval  18059  lubfval  18077  glbfval  18090  joinfval  18100  meetfval  18114  odujoin  18135  odumeet  18137  ipole  18261  eqgval  18814  unitpropd  19948  znleval  20771  ltbval  21253  opsrval  21256  lmbr  22418  metustexhalf  23721  metucn  23736  isphtpc  24166  taylthlem1  25541  ulmval  25548  tgjustf  26843  iscgrg  26882  legov  26955  ishlg  26972  opphllem5  27121  opphllem6  27122  hpgbr  27130  iscgra  27179  acopy  27203  isinag  27208  isleag  27217  iseqlg  27237  wlkonprop  28035  wksonproplem  28081  wksonproplemOLD  28082  istrlson  28084  upgrwlkdvspth  28116  ispthson  28119  isspthson  28120  cyclispthon  28178  wspthsn  28222  wspthsnon  28226  iswspthsnon  28230  1pthon2v  28526  3wlkond  28544  dfconngr1  28561  isconngr  28562  isconngr1  28563  1conngr  28567  conngrv2edg  28568  minvecolem4b  29249  minvecolem4  29251  br8d  30959  ressprs  31250  resstos  31254  mntoval  31269  mgcoval  31273  mgcval  31274  isomnd  31336  submomnd  31345  ogrpaddltrd  31354  isinftm  31444  isorng  31507  rprmval  31673  metidv  31851  pstmfval  31855  faeval  32223  brfae  32225  isacycgr  33116  isacycgr1  33117  issconn  33197  satfbrsuc  33337  mclsax  33540  bj-imdirval3  35364  unceq  35763  alrmomodm  36498  relbrcoss  36571  lcvbr  37042  isopos  37201  cmtvalN  37232  isoml  37259  cvrfval  37289  cvrval  37290  pats  37306  isatl  37320  iscvlat  37344  ishlat1  37373  llnset  37526  lplnset  37550  lvolset  37593  lineset  37759  psubspset  37765  pmapfval  37777  lautset  38103  ldilfset  38129  ltrnfset  38138  trlfset  38181  diaffval  39051  dicffval  39195  dihffval  39251  prjspnvs  40466  fnwe2lem2  40883  fnwe2lem3  40884  aomclem8  40893  brfvid  41302  brfvidRP  41303  brfvrcld  41306  brfvrcld2  41307  iunrelexpuztr  41334  brtrclfv2  41342  neicvgnvor  41733  neicvgel1  41736  fperdvper  43467  upwlkbprop  45311  rngcifuestrc  45566  isprsd  46260  lubeldm2d  46263  glbeldm2d  46264  catprsc  46305  catprsc2  46306  prsthinc  46346  prstcle  46362