Theorem breqd 5118

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-br 5108

This theorem is referenced by:  breq123d  5121  breqdi  5122  sbcbr123  5161  sbcbr  5162  sbcbr12g  5163  fvmptopab  7443  fvmptopabOLD  7444  brfvopab  7446  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  mptmpoopabovd  8061  mptmpoopabbrdOLDOLD  8062  mptmpoopabovdOLD  8063  bropopvvv  8069  bropfvvvvlem  8070  sprmpod  8203  fprlem1  8279  supeq123d  9401  frrlem15  9710  fpwwe2lem11  10594  fpwwe2  10596  brtrclfv  14968  dfrtrclrec2  15024  rtrclreclem3  15026  relexpindlem  15029  shftfib  15038  2shfti  15046  prdsval  17418  pwsle  17455  pwsleval  17456  imasleval  17504  issect  17715  isinv  17722  brcic  17760  ciclcl  17764  cicrcl  17765  isfunc  17826  funcres2c  17865  isfull  17874  isfth  17878  fullpropd  17884  fthpropd  17885  elhoma  17994  isposd  18283  pltval  18291  lubfval  18309  glbfval  18322  joinfval  18332  meetfval  18346  odujoin  18367  odumeet  18369  ipole  18493  eqgval  19109  unitpropd  20326  rngcifuestrc  20548  znleval  21464  ltbval  21950  opsrval  21953  lmbr  23145  metustexhalf  24444  metucn  24459  isphtpc  24893  taylthlem1  26281  ulmval  26289  tgjustf  28400  iscgrg  28439  legov  28512  ishlg  28529  opphllem5  28678  opphllem6  28679  hpgbr  28687  iscgra  28736  acopy  28760  isinag  28765  isleag  28774  iseqlg  28794  wlkonprop  29586  wksonproplem  29632  wksonproplemOLD  29633  istrlson  29635  upgrwlkdvspth  29669  ispthson  29672  isspthson  29673  cyclispthon  29734  wspthsn  29778  wspthsnon  29782  iswspthsnon  29786  1pthon2v  30082  3wlkond  30100  dfconngr1  30117  isconngr  30118  isconngr1  30119  1conngr  30123  conngrv2edg  30124  minvecolem4b  30807  minvecolem4  30809  br8d  32538  ressprs  32890  resstos  32893  mntoval  32908  mgcoval  32912  mgcval  32913  isomnd  33015  submomnd  33024  ogrpaddltrd  33033  isinftm  33135  isorng  33277  rprmval  33487  metidv  33882  pstmfval  33886  faeval  34236  brfae  34238  isacycgr  35132  isacycgr1  35133  issconn  35213  satfbrsuc  35353  mclsax  35556  weiunpo  36453  weiunfr  36455  bj-imdirval3  37172  unceq  37591  alrmomodm  38341  relbrcoss  38437  lcvbr  39014  isopos  39173  cmtvalN  39204  isoml  39231  cvrfval  39261  cvrval  39262  pats  39278  isatl  39292  iscvlat  39316  ishlat1  39345  llnset  39499  lplnset  39523  lvolset  39566  lineset  39732  psubspset  39738  pmapfval  39750  lautset  40076  ldilfset  40102  ltrnfset  40111  trlfset  40154  diaffval  41024  dicffval  41168  dihffval  41224  prjspnvs  42608  fnwe2lem2  43040  fnwe2lem3  43041  aomclem8  43050  brfvid  43676  brfvidRP  43677  brfvrcld  43680  brfvrcld2  43681  iunrelexpuztr  43708  brtrclfv2  43716  neicvgnvor  44105  neicvgel1  44108  fperdvper  45917  upwlkbprop  48126  isprsd  48943  lubeldm2d  48946  glbeldm2d  48947  catprsc  49002  catprsc2  49003  oppccicb  49040  funcoppc2  49132  uptpos  49187  prsthinc  49453  prstcle  49545  lanup  49630  ranup  49631  islmd  49654  cmddu  49657  lmdran  49660  cmdlan  49661