Theorem breqd 5177

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-br 5167

This theorem is referenced by:  breq123d  5180  breqdi  5181  sbcbr123  5220  sbcbr  5221  sbcbr12g  5222  fvmptopab  7504  fvmptopabOLD  7505  brfvopab  7507  mptmpoopabbrd  8121  mptmpoopabbrdOLD  8122  mptmpoopabovd  8123  mptmpoopabbrdOLDOLD  8124  mptmpoopabovdOLD  8125  bropopvvv  8131  bropfvvvvlem  8132  sprmpod  8265  fprlem1  8341  wfrlem5OLD  8369  supeq123d  9519  frrlem15  9826  fpwwe2lem11  10710  fpwwe2  10712  brtrclfv  15051  dfrtrclrec2  15107  rtrclreclem3  15109  relexpindlem  15112  shftfib  15121  2shfti  15129  prdsval  17515  pwsle  17552  pwsleval  17553  imasleval  17601  issect  17814  isinv  17821  brcic  17859  ciclcl  17863  cicrcl  17864  isfunc  17928  funcres2c  17968  isfull  17977  isfth  17981  fullpropd  17987  fthpropd  17988  elhoma  18099  isposd  18393  pltval  18402  lubfval  18420  glbfval  18433  joinfval  18443  meetfval  18457  odujoin  18478  odumeet  18480  ipole  18604  eqgval  19217  unitpropd  20443  rngcifuestrc  20661  znleval  21596  ltbval  22084  opsrval  22087  lmbr  23287  metustexhalf  24590  metucn  24605  isphtpc  25045  taylthlem1  26433  ulmval  26441  tgjustf  28499  iscgrg  28538  legov  28611  ishlg  28628  opphllem5  28777  opphllem6  28778  hpgbr  28786  iscgra  28835  acopy  28859  isinag  28864  isleag  28873  iseqlg  28893  wlkonprop  29694  wksonproplem  29740  wksonproplemOLD  29741  istrlson  29743  upgrwlkdvspth  29775  ispthson  29778  isspthson  29779  cyclispthon  29837  wspthsn  29881  wspthsnon  29885  iswspthsnon  29889  1pthon2v  30185  3wlkond  30203  dfconngr1  30220  isconngr  30221  isconngr1  30222  1conngr  30226  conngrv2edg  30227  minvecolem4b  30910  minvecolem4  30912  br8d  32632  ressprs  32936  resstos  32940  mntoval  32955  mgcoval  32959  mgcval  32960  isomnd  33051  submomnd  33060  ogrpaddltrd  33069  isinftm  33161  isorng  33294  rprmval  33509  metidv  33838  pstmfval  33842  faeval  34210  brfae  34212  isacycgr  35113  isacycgr1  35114  issconn  35194  satfbrsuc  35334  mclsax  35537  weiunpo  36431  weiunfr  36433  bj-imdirval3  37150  unceq  37557  alrmomodm  38315  relbrcoss  38402  lcvbr  38977  isopos  39136  cmtvalN  39167  isoml  39194  cvrfval  39224  cvrval  39225  pats  39241  isatl  39255  iscvlat  39279  ishlat1  39308  llnset  39462  lplnset  39486  lvolset  39529  lineset  39695  psubspset  39701  pmapfval  39713  lautset  40039  ldilfset  40065  ltrnfset  40074  trlfset  40117  diaffval  40987  dicffval  41131  dihffval  41187  prjspnvs  42575  fnwe2lem2  43008  fnwe2lem3  43009  aomclem8  43018  brfvid  43649  brfvidRP  43650  brfvrcld  43653  brfvrcld2  43654  iunrelexpuztr  43681  brtrclfv2  43689  neicvgnvor  44078  neicvgel1  44081  fperdvper  45840  upwlkbprop  47861  isprsd  48635  lubeldm2d  48638  glbeldm2d  48639  catprsc  48680  catprsc2  48681  prsthinc  48721  prstcle  48737