Theorem breqd 5085

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   class class class wbr 5074

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-clel 2810  df-br 5075

This theorem is referenced by:  breq123d  5088  breqdi  5089  sbcbr123  5128  sbcbr  5129  sbcbr12g  5130  fvmptopab  7411  brfvopab  7413  mptmpoopabbrd  8022  mptmpoopabovd  8023  bropopvvv  8029  bropfvvvvlem  8030  sprmpod  8163  fprlem1  8239  supeq123d  9352  frrlem15  9670  fpwwe2lem11  10553  fpwwe2  10555  brtrclfv  14953  dfrtrclrec2  15009  rtrclreclem3  15011  relexpindlem  15014  shftfib  15023  2shfti  15031  prdsval  17407  pwsle  17445  pwsleval  17446  imasleval  17494  issect  17709  isinv  17716  brcic  17754  ciclcl  17758  cicrcl  17759  isfunc  17820  funcres2c  17859  isfull  17868  isfth  17872  fullpropd  17878  fthpropd  17879  elhoma  17988  isposd  18277  pltval  18285  lubfval  18303  glbfval  18316  joinfval  18326  meetfval  18340  odujoin  18361  odumeet  18363  resstos  18385  ipole  18489  eqgval  19141  isomnd  20087  submomnd  20096  ogrpaddltrd  20104  unitpropd  20386  rngcifuestrc  20605  isorng  20827  znleval  21523  ltbval  22010  opsrval  22013  lmbr  23211  metustexhalf  24509  metucn  24524  isphtpc  24949  taylthlem1  26326  ulmval  26333  tgjustf  28529  iscgrg  28568  legov  28641  ishlg  28658  opphllem5  28807  opphllem6  28808  hpgbr  28816  iscgra  28865  acopy  28889  isinag  28894  isleag  28903  iseqlg  28923  wlkonprop  29713  wksonproplem  29759  istrlson  29761  upgrwlkdvspth  29795  ispthson  29798  isspthson  29799  cyclispthon  29860  wspthsn  29904  wspthsnon  29908  iswspthsnon  29912  1pthon2v  30211  3wlkond  30229  dfconngr1  30246  isconngr  30247  isconngr1  30248  1conngr  30252  conngrv2edg  30253  minvecolem4b  30937  minvecolem4  30939  br8d  32669  ressprs  33014  mntoval  33030  mgcoval  33034  mgcval  33035  isinftm  33230  rprmval  33564  metidv  34024  pstmfval  34028  faeval  34378  brfae  34380  isacycgr  35315  isacycgr1  35316  issconn  35396  satfbrsuc  35536  mclsax  35739  weiunpo  36635  weiunfr  36637  bj-imdirval3  37486  unceq  37906  alrmomodm  38668  relbrcoss  38845  lcvbr  39455  isopos  39614  cmtvalN  39645  isoml  39672  cvrfval  39702  cvrval  39703  pats  39719  isatl  39733  iscvlat  39757  ishlat1  39786  llnset  39939  lplnset  39963  lvolset  40006  lineset  40172  psubspset  40178  pmapfval  40190  lautset  40516  ldilfset  40542  ltrnfset  40551  trlfset  40594  diaffval  41464  dicffval  41608  dihffval  41664  prjspnvs  43041  fnwe2lem2  43467  fnwe2lem3  43468  aomclem8  43477  brfvid  44102  brfvidRP  44103  brfvrcld  44106  brfvrcld2  44107  iunrelexpuztr  44134  brtrclfv2  44142  neicvgnvor  44531  neicvgel1  44534  fperdvper  46335  upwlkbprop  48602  isprsd  49418  lubeldm2d  49421  glbeldm2d  49422  catprsc  49476  catprsc2  49477  oppccicb  49514  funcoppc2  49606  uptpos  49661  prsthinc  49927  prstcle  50019  lanup  50104  ranup  50105  islmd  50128  cmddu  50131  lmdran  50134  cmdlan  50135