Theorem breqd 5041

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   class class class wbr 5030

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-br 5031

This theorem is referenced by:  breq123d  5044  breqdi  5045  sbcbr123  5084  sbcbr  5085  sbcbr12g  5086  fvmptopab  7188  brfvopab  7190  mptmpoopabbrd  7761  mptmpoopabovd  7762  bropopvvv  7768  bropfvvvvlem  7769  sprmpod  7873  wfrlem5  7942  supeq123d  8898  fpwwe2lem12  10052  fpwwe2  10054  brtrclfv  14353  dfrtrclrec2  14409  rtrclreclem3  14411  relexpindlem  14414  shftfib  14423  2shfti  14431  prdsval  16720  pwsle  16757  pwsleval  16758  imasleval  16806  issect  17015  isinv  17022  brcic  17060  ciclcl  17064  cicrcl  17065  isfunc  17126  funcres2c  17163  isfull  17172  isfth  17176  fullpropd  17182  fthpropd  17183  elhoma  17284  isposd  17557  pltval  17562  lubfval  17580  glbfval  17593  joinfval  17603  meetfval  17617  odumeet  17742  odujoin  17744  ipole  17760  eqgval  18321  unitpropd  19443  znleval  20246  ltbval  20711  opsrval  20714  lmbr  21863  metustexhalf  23163  metucn  23178  isphtpc  23599  taylthlem1  24968  ulmval  24975  tgjustf  26267  iscgrg  26306  legov  26379  ishlg  26396  opphllem5  26545  opphllem6  26546  hpgbr  26554  iscgra  26603  acopy  26627  isinag  26632  isleag  26641  iseqlg  26661  wlkonprop  27448  wksonproplem  27494  istrlson  27496  upgrwlkdvspth  27528  ispthson  27531  isspthson  27532  cyclispthon  27590  wspthsn  27634  wspthsnon  27638  iswspthsnon  27642  1pthon2v  27938  3wlkond  27956  dfconngr1  27973  isconngr  27974  isconngr1  27975  1conngr  27979  conngrv2edg  27980  minvecolem4b  28661  minvecolem4  28663  br8d  30374  ressprs  30668  resstos  30673  mntoval  30690  mgcoval  30694  mgcval  30695  isomnd  30752  submomnd  30761  ogrpaddltrd  30770  isinftm  30860  isorng  30923  rprmval  31072  metidv  31245  pstmfval  31249  faeval  31615  brfae  31617  isacycgr  32505  isacycgr1  32506  issconn  32586  satfbrsuc  32726  mclsax  32929  fprlem1  33250  frrlem15  33255  bj-imdirval3  34599  unceq  35034  alrmomodm  35773  relbrcoss  35846  lcvbr  36317  isopos  36476  cmtvalN  36507  isoml  36534  cvrfval  36564  cvrval  36565  pats  36581  isatl  36595  iscvlat  36619  ishlat1  36648  llnset  36801  lplnset  36825  lvolset  36868  lineset  37034  psubspset  37040  pmapfval  37052  lautset  37378  ldilfset  37404  ltrnfset  37413  trlfset  37456  diaffval  38326  dicffval  38470  dihffval  38526  fnwe2lem2  39995  fnwe2lem3  39996  aomclem8  40005  brfvid  40388  brfvidRP  40389  brfvrcld  40392  brfvrcld2  40393  iunrelexpuztr  40420  brtrclfv2  40428  neicvgnvor  40819  neicvgel1  40822  fperdvper  42561  upwlkbprop  44366  rngcifuestrc  44621