Theorem breqd 5121

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804  df-br 5111

This theorem is referenced by:  breq123d  5124  breqdi  5125  sbcbr123  5164  sbcbr  5165  sbcbr12g  5166  fvmptopab  7446  fvmptopabOLD  7447  brfvopab  7449  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  mptmpoopabovd  8064  mptmpoopabbrdOLDOLD  8065  mptmpoopabovdOLD  8066  bropopvvv  8072  bropfvvvvlem  8073  sprmpod  8206  fprlem1  8282  supeq123d  9408  frrlem15  9717  fpwwe2lem11  10601  fpwwe2  10603  brtrclfv  14975  dfrtrclrec2  15031  rtrclreclem3  15033  relexpindlem  15036  shftfib  15045  2shfti  15053  prdsval  17425  pwsle  17462  pwsleval  17463  imasleval  17511  issect  17722  isinv  17729  brcic  17767  ciclcl  17771  cicrcl  17772  isfunc  17833  funcres2c  17872  isfull  17881  isfth  17885  fullpropd  17891  fthpropd  17892  elhoma  18001  isposd  18290  pltval  18298  lubfval  18316  glbfval  18329  joinfval  18339  meetfval  18353  odujoin  18374  odumeet  18376  ipole  18500  eqgval  19116  unitpropd  20333  rngcifuestrc  20555  znleval  21471  ltbval  21957  opsrval  21960  lmbr  23152  metustexhalf  24451  metucn  24466  isphtpc  24900  taylthlem1  26288  ulmval  26296  tgjustf  28407  iscgrg  28446  legov  28519  ishlg  28536  opphllem5  28685  opphllem6  28686  hpgbr  28694  iscgra  28743  acopy  28767  isinag  28772  isleag  28781  iseqlg  28801  wlkonprop  29593  wksonproplem  29639  wksonproplemOLD  29640  istrlson  29642  upgrwlkdvspth  29676  ispthson  29679  isspthson  29680  cyclispthon  29741  wspthsn  29785  wspthsnon  29789  iswspthsnon  29793  1pthon2v  30089  3wlkond  30107  dfconngr1  30124  isconngr  30125  isconngr1  30126  1conngr  30130  conngrv2edg  30131  minvecolem4b  30814  minvecolem4  30816  br8d  32545  ressprs  32897  resstos  32900  mntoval  32915  mgcoval  32919  mgcval  32920  isomnd  33022  submomnd  33031  ogrpaddltrd  33040  isinftm  33142  isorng  33284  rprmval  33494  metidv  33889  pstmfval  33893  faeval  34243  brfae  34245  isacycgr  35139  isacycgr1  35140  issconn  35220  satfbrsuc  35360  mclsax  35563  weiunpo  36460  weiunfr  36462  bj-imdirval3  37179  unceq  37598  alrmomodm  38348  relbrcoss  38444  lcvbr  39021  isopos  39180  cmtvalN  39211  isoml  39238  cvrfval  39268  cvrval  39269  pats  39285  isatl  39299  iscvlat  39323  ishlat1  39352  llnset  39506  lplnset  39530  lvolset  39573  lineset  39739  psubspset  39745  pmapfval  39757  lautset  40083  ldilfset  40109  ltrnfset  40118  trlfset  40161  diaffval  41031  dicffval  41175  dihffval  41231  prjspnvs  42615  fnwe2lem2  43047  fnwe2lem3  43048  aomclem8  43057  brfvid  43683  brfvidRP  43684  brfvrcld  43687  brfvrcld2  43688  iunrelexpuztr  43715  brtrclfv2  43723  neicvgnvor  44112  neicvgel1  44115  fperdvper  45924  upwlkbprop  48130  isprsd  48947  lubeldm2d  48950  glbeldm2d  48951  catprsc  49006  catprsc2  49007  oppccicb  49044  funcoppc2  49136  uptpos  49191  prsthinc  49457  prstcle  49549  lanup  49634  ranup  49635  islmd  49658  cmddu  49661  lmdran  49664  cmdlan  49665