Theorem breqd 5101

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1550   class class class wbr 5090

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-cleq 2744  df-clel 2827  df-br 5091

This theorem is referenced by:  breq123d  5104  breqdi  5105  sbcbr123  5144  sbcbr  5145  sbcbr12g  5146  fvmptopab  7436  brfvopab  7438  mptmpoopabbrd  8046  mptmpoopabovd  8047  bropopvvv  8053  bropfvvvvlem  8054  sprmpod  8188  fprlem1  8265  supeq123d  9382  frrlem15  9701  fpwwe2lem11  10585  fpwwe2  10587  brtrclfv  15001  dfrtrclrec2  15057  rtrclreclem3  15059  relexpindlem  15062  shftfib  15071  2shfti  15079  prdsval  17456  pwsle  17494  pwsleval  17495  imasleval  17543  issect  17758  isinv  17765  brcic  17803  ciclcl  17807  cicrcl  17808  isfunc  17869  funcres2c  17908  isfull  17917  isfth  17921  fullpropd  17927  fthpropd  17928  elhoma  18037  isposd  18326  pltval  18334  lubfval  18352  glbfval  18365  joinfval  18375  meetfval  18389  odujoin  18410  odumeet  18412  resstos  18434  ipole  18538  eqgval  19190  isomnd  20135  submomnd  20144  ogrpaddltrd  20152  unitpropd  20434  rngcifuestrc  20657  isorng  20879  znleval  21575  ltbval  22065  opsrval  22068  lmbr  23287  metustexhalf  24585  metucn  24600  isphtpc  25025  taylthlem1  26402  ulmval  26409  tgjustf  28608  iscgrg  28647  legov  28720  ishlg  28737  opphllem5  28886  opphllem6  28887  hpgbr  28895  iscgra  28944  acopy  28968  isinag  28973  isleag  28982  iseqlg  29002  wlkonprop  29792  wksonproplem  29838  istrlson  29840  upgrwlkdvspth  29874  ispthson  29877  isspthson  29878  cyclispthon  29939  wspthsn  29983  wspthsnon  29987  iswspthsnon  29991  1pthon2v  30290  3wlkond  30308  dfconngr1  30325  isconngr  30326  isconngr1  30327  1conngr  30331  conngrv2edg  30332  minvecolem4b  31016  minvecolem4  31018  br8d  32749  ressprs  33094  mntoval  33110  mgcoval  33114  mgcval  33115  isinftm  33311  rprmval  33656  metidv  34133  pstmfval  34137  faeval  34487  brfae  34489  isacycgr  35433  isacycgr1  35434  issconn  35514  satfbrsuc  35654  mclsax  35857  weiunpo  36763  weiunfr  36765  bj-imdirval3  37614  unceq  38034  alrmomodm  38796  relbrcoss  38973  lcvbr  39583  isopos  39742  cmtvalN  39773  isoml  39800  cvrfval  39830  cvrval  39831  pats  39847  isatl  39861  iscvlat  39885  ishlat1  39914  llnset  40067  lplnset  40091  lvolset  40134  lineset  40300  psubspset  40306  pmapfval  40318  lautset  40644  ldilfset  40670  ltrnfset  40679  trlfset  40722  diaffval  41592  dicffval  41736  dihffval  41792  prjspnvs  43140  fnwe2lem2  43566  fnwe2lem3  43567  aomclem8  43576  brfvid  44201  brfvidRP  44202  brfvrcld  44205  brfvrcld2  44206  iunrelexpuztr  44233  brtrclfv2  44241  neicvgnvor  44630  neicvgel1  44633  fperdvper  46431  upwlkbprop  48698  isprsd  49514  lubeldm2d  49517  glbeldm2d  49518  catprsc  49572  catprsc2  49573  oppccicb  49610  funcoppc2  49702  uptpos  49757  prsthinc  50023  prstcle  50115  lanup  50200  ranup  50201  islmd  50224  cmddu  50227  lmdran  50230  cmdlan  50231