Theorem breqd 5119

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569   class class class wbr 5108

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-clel 2837  df-br 5109

This theorem is used by:  breq123d  5122  breqdi  5123  sbcbr123  5164  sbcbr  5165  sbcbr12g  5166  fvmptopab  7467  brfvopab  7469  mptmpoopabbrd  8076  mptmpoopabovd  8077  bropopvvv  8083  bropfvvvvlem  8084  sprmpod  8218  fprlem1  8295  supeq123d  9408  frrlem15  9727  fpwwe2lem11  10632  fpwwe2  10634  brtrclfv  15046  dfrtrclrec2  15102  rtrclreclem3  15104  relexpindlem  15107  shftfib  15116  2shfti  15124  prdsval  17514  pwsle  17552  pwsleval  17553  imasleval  17601  issect  17816  isinv  17823  brcic  17861  ciclcl  17865  cicrcl  17866  isfunc  17927  funcres2c  17966  isfull  17975  isfth  17979  fullpropd  17985  fthpropd  17986  elhoma  18095  isposd  18384  pltval  18392  lubfval  18410  glbfval  18423  joinfval  18433  meetfval  18447  odujoin  18468  odumeet  18470  resstos  18492  ipole  18596  eqgval  19251  isomnd  20199  submomnd  20208  ogrpaddltrd  20216  unitpropd  20506  rngcifuestrc  20749  isorng  20975  znleval  21715  ltbval  22205  opsrval  22208  lmbr  23426  metustexhalf  24724  metucn  24739  isphtpc  25164  taylthlem1  26547  ulmval  26554  tgjustf  28753  iscgrg  28792  legov  28865  ishlg2  28882  ishlg  28885  opphllem5  29043  opphllem6  29044  hpgbr  29053  tgplnfn  29068  plngval  29070  isplng  29071  iscgra  29131  acopy  29155  isinag  29166  isleag  29175  iseqlg  29195  dfprlng3  29209  wlkonprop  30017  wksonproplem  30063  istrlson  30065  upgrwlkdvspth  30099  ispthson  30102  isspthson  30103  cyclispthon  30164  wspthsn  30208  wspthsnon  30212  iswspthsnon  30216  1pthon2v  30515  3wlkond  30533  dfconngr1  30550  isconngr  30551  isconngr1  30552  1conngr  30556  conngrv2edg  30557  minvecolem4b  31241  minvecolem4  31243  br8d  32964  ressprs  33295  mntoval  33311  mgcoval  33315  mgcval  33316  isinftm  33510  rprmval  33815  metidv  34291  pstmfval  34295  faeval  34645  brfae  34647  isacycgr  35645  isacycgr1  35646  issconn  35726  satfbrsuc  35866  mclsax  36069  weiunpo  37004  weiunfr  37006  bj-imdirval3  37856  unceq  38276  alrmomodm  39036  relbrcoss  39213  lcvbr  39823  isopos  39982  cmtvalN  40013  isoml  40040  cvrfval  40070  cvrval  40071  pats  40087  isatl  40101  iscvlat  40125  ishlat1  40154  llnset  40307  lplnset  40331  lvolset  40374  lineset  40540  psubspset  40546  pmapfval  40558  lautset  40884  ldilfset  40910  ltrnfset  40919  trlfset  40962  diaffval  41832  dicffval  41976  dihffval  42032  prjspnvs  43380  fnwe2lem2  43806  fnwe2lem3  43807  aomclem8  43816  brfvid  44441  brfvidRP  44442  brfvrcld  44445  brfvrcld2  44446  iunrelexpuztr  44473  brtrclfv2  44481  neicvgnvor  44870  neicvgel1  44873  fperdvper  46661  upwlkbprop  48931  isprsd  49761  lubeldm2d  49764  glbeldm2d  49765  catprsc  49819  catprsc2  49820  oppccicb  49857  funcoppc2  49949  uptpos  50004  prsthinc  50270  prstcle  50362  lanup  50447  ranup  50448  islmd  50471  cmddu  50474  lmdran  50477  cmdlan  50478