Theorem breqd 5116

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   class class class wbr 5105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-clel 2840  df-br 5106

This theorem is referenced by:  breq123d  5119  breqdi  5120  sbcbr123  5159  sbcbr  5160  sbcbr12g  5161  fvmptopab  7455  brfvopab  7457  mptmpoopabbrd  8066  mptmpoopabovd  8067  bropopvvv  8073  bropfvvvvlem  8074  sprmpod  8208  fprlem1  8285  supeq123d  9398  frrlem15  9717  fpwwe2lem11  10614  fpwwe2  10616  brtrclfv  15029  dfrtrclrec2  15085  rtrclreclem3  15087  relexpindlem  15090  shftfib  15099  2shfti  15107  prdsval  17498  pwsle  17536  pwsleval  17537  imasleval  17585  issect  17800  isinv  17807  brcic  17845  ciclcl  17849  cicrcl  17850  isfunc  17911  funcres2c  17950  isfull  17959  isfth  17963  fullpropd  17969  fthpropd  17970  elhoma  18079  isposd  18368  pltval  18376  lubfval  18394  glbfval  18407  joinfval  18417  meetfval  18431  odujoin  18452  odumeet  18454  resstos  18476  ipole  18580  eqgval  19236  isomnd  20184  submomnd  20193  ogrpaddltrd  20201  unitpropd  20490  rngcifuestrc  20715  isorng  20933  znleval  21664  ltbval  22154  opsrval  22157  lmbr  23376  metustexhalf  24674  metucn  24689  isphtpc  25114  taylthlem1  26494  ulmval  26501  tgjustf  28700  iscgrg  28739  legov  28812  ishlg  28829  opphllem5  28982  opphllem6  28983  hpgbr  28991  tgplnfn  29005  plngval  29007  isplng  29008  iscgra  29061  acopy  29085  isinag  29090  isleag  29099  iseqlg  29119  wlkonprop  29915  wksonproplem  29961  istrlson  29963  upgrwlkdvspth  29997  ispthson  30000  isspthson  30001  cyclispthon  30062  wspthsn  30106  wspthsnon  30110  iswspthsnon  30114  1pthon2v  30413  3wlkond  30431  dfconngr1  30448  isconngr  30449  isconngr1  30450  1conngr  30454  conngrv2edg  30455  minvecolem4b  31139  minvecolem4  31141  br8d  32865  ressprs  33199  mntoval  33215  mgcoval  33219  mgcval  33220  isinftm  33414  rprmval  33723  metidv  34199  pstmfval  34203  faeval  34553  brfae  34555  isacycgr  35508  isacycgr1  35509  issconn  35589  satfbrsuc  35729  mclsax  35932  weiunpo  36838  weiunfr  36840  bj-imdirval3  37688  unceq  38108  alrmomodm  38870  relbrcoss  39047  lcvbr  39657  isopos  39816  cmtvalN  39847  isoml  39874  cvrfval  39904  cvrval  39905  pats  39921  isatl  39935  iscvlat  39959  ishlat1  39988  llnset  40141  lplnset  40165  lvolset  40208  lineset  40374  psubspset  40380  pmapfval  40392  lautset  40718  ldilfset  40744  ltrnfset  40753  trlfset  40796  diaffval  41666  dicffval  41810  dihffval  41866  prjspnvs  43214  fnwe2lem2  43640  fnwe2lem3  43641  aomclem8  43650  brfvid  44275  brfvidRP  44276  brfvrcld  44279  brfvrcld2  44280  iunrelexpuztr  44307  brtrclfv2  44315  neicvgnvor  44704  neicvgel1  44707  fperdvper  46491  upwlkbprop  48758  isprsd  49584  lubeldm2d  49587  glbeldm2d  49588  catprsc  49642  catprsc2  49643  oppccicb  49680  funcoppc2  49772  uptpos  49827  prsthinc  50093  prstcle  50185  lanup  50270  ranup  50271  islmd  50294  cmddu  50297  lmdran  50300  cmdlan  50301