Theorem breqd 4696

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523   class class class wbr 4685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647  df-br 4686

This theorem is referenced by:  breq123d  4699  breqdi  4700  sbcbr123  4739  sbcbr  4740  sbcbr12g  4741  fvmptopab  6739  brfvopab  6742  mptmpt2opabbrd  7293  mptmpt2opabovd  7294  bropopvvv  7300  bropfvvvvlem  7301  sprmpt2d  7395  wfrlem5  7464  supeq123d  8397  fpwwe2lem12  9501  fpwwe2  9503  brtrclfv  13787  dfrtrclrec2  13841  rtrclreclem3  13844  relexpindlem  13847  shftfib  13856  2shfti  13864  prdsval  16162  pwsle  16199  pwsleval  16200  imasleval  16248  issect  16460  isinv  16467  episect  16492  brcic  16505  ciclcl  16509  cicrcl  16510  isfunc  16571  funcres2c  16608  isfull  16617  isfth  16621  fullpropd  16627  fthpropd  16628  elhoma  16729  isposd  17002  pltval  17007  lubfval  17025  glbfval  17038  joinfval  17048  meetfval  17062  odumeet  17187  odujoin  17189  ipole  17205  eqgval  17690  unitpropd  18743  ltbval  19519  opsrval  19522  znleval  19951  lmbr  21110  metustexhalf  22408  metucn  22423  isphtpc  22840  dvef  23788  taylthlem1  24172  ulmval  24179  iscgrg  25452  legov  25525  ishlg  25542  opphllem5  25688  opphllem6  25689  hpgbr  25697  iscgra  25746  acopy  25769  acopyeu  25770  isinag  25774  isleag  25778  iseqlg  25792  wlkonprop  26610  wksonproplem  26657  istrlson  26659  upgrwlkdvspth  26691  ispthson  26694  isspthson  26695  cyclispthon  26752  wspthsn  26797  wspthsnon  26801  iswspthsnon  26806  iswspthsnonOLD  26807  1pthon2v  27131  3wlkond  27149  dfconngr1  27166  isconngr  27167  isconngr1  27168  1conngr  27172  conngrv2edg  27173  minvecolem4b  27862  minvecolem4  27864  br8d  29548  ressprs  29783  resstos  29788  isomnd  29829  submomnd  29838  ogrpaddltrd  29848  isinftm  29863  isorng  29927  metidv  30063  pstmfval  30067  faeval  30437  brfae  30439  issconn  31334  mclsax  31592  frrlem5  31909  unceq  33516  alrmomodm  34264  relbrcoss  34336  lcvbr  34626  isopos  34785  cmtvalN  34816  isoml  34843  cvrfval  34873  cvrval  34874  pats  34890  isatl  34904  iscvlat  34928  ishlat1  34957  llnset  35109  lplnset  35133  lvolset  35176  lineset  35342  psubspset  35348  pmapfval  35360  lautset  35686  ldilfset  35712  ltrnfset  35721  trlfset  35765  diaffval  36636  dicffval  36780  dihffval  36836  fnwe2lem2  37938  fnwe2lem3  37939  aomclem8  37948  brfvid  38296  brfvidRP  38297  brfvrcld  38300  brfvrcld2  38301  iunrelexpuztr  38328  brtrclfv2  38336  neicvgnvor  38731  neicvgel1  38734  fperdvper  40451  upwlkbprop  42044  rngcifuestrc  42322