Theorem breqd 5097

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-br 5087

This theorem is referenced by:  breq123d  5100  breqdi  5101  sbcbr123  5140  sbcbr  5141  sbcbr12g  5142  fvmptopab  7422  brfvopab  7424  mptmpoopabbrd  8033  mptmpoopabovd  8034  bropopvvv  8040  bropfvvvvlem  8041  sprmpod  8174  fprlem1  8250  supeq123d  9363  frrlem15  9681  fpwwe2lem11  10564  fpwwe2  10566  brtrclfv  14964  dfrtrclrec2  15020  rtrclreclem3  15022  relexpindlem  15025  shftfib  15034  2shfti  15042  prdsval  17418  pwsle  17456  pwsleval  17457  imasleval  17505  issect  17720  isinv  17727  brcic  17765  ciclcl  17769  cicrcl  17770  isfunc  17831  funcres2c  17870  isfull  17879  isfth  17883  fullpropd  17889  fthpropd  17890  elhoma  17999  isposd  18288  pltval  18296  lubfval  18314  glbfval  18327  joinfval  18337  meetfval  18351  odujoin  18372  odumeet  18374  resstos  18396  ipole  18500  eqgval  19152  isomnd  20098  submomnd  20107  ogrpaddltrd  20115  unitpropd  20397  rngcifuestrc  20616  isorng  20838  znleval  21534  ltbval  22021  opsrval  22024  lmbr  23223  metustexhalf  24521  metucn  24536  isphtpc  24961  taylthlem1  26338  ulmval  26345  tgjustf  28541  iscgrg  28580  legov  28653  ishlg  28670  opphllem5  28819  opphllem6  28820  hpgbr  28828  iscgra  28877  acopy  28901  isinag  28906  isleag  28915  iseqlg  28935  wlkonprop  29725  wksonproplem  29771  istrlson  29773  upgrwlkdvspth  29807  ispthson  29810  isspthson  29811  cyclispthon  29872  wspthsn  29916  wspthsnon  29920  iswspthsnon  29924  1pthon2v  30223  3wlkond  30241  dfconngr1  30258  isconngr  30259  isconngr1  30260  1conngr  30264  conngrv2edg  30265  minvecolem4b  30949  minvecolem4  30951  br8d  32681  ressprs  33026  mntoval  33042  mgcoval  33046  mgcval  33047  isinftm  33242  rprmval  33576  metidv  34036  pstmfval  34040  faeval  34390  brfae  34392  isacycgr  35327  isacycgr1  35328  issconn  35408  satfbrsuc  35548  mclsax  35751  weiunpo  36647  weiunfr  36649  bj-imdirval3  37498  unceq  37918  alrmomodm  38680  relbrcoss  38857  lcvbr  39467  isopos  39626  cmtvalN  39657  isoml  39684  cvrfval  39714  cvrval  39715  pats  39731  isatl  39745  iscvlat  39769  ishlat1  39798  llnset  39951  lplnset  39975  lvolset  40018  lineset  40184  psubspset  40190  pmapfval  40202  lautset  40528  ldilfset  40554  ltrnfset  40563  trlfset  40606  diaffval  41476  dicffval  41620  dihffval  41676  prjspnvs  43053  fnwe2lem2  43479  fnwe2lem3  43480  aomclem8  43489  brfvid  44114  brfvidRP  44115  brfvrcld  44118  brfvrcld2  44119  iunrelexpuztr  44146  brtrclfv2  44154  neicvgnvor  44543  neicvgel1  44546  fperdvper  46347  upwlkbprop  48608  isprsd  49424  lubeldm2d  49427  glbeldm2d  49428  catprsc  49482  catprsc2  49483  oppccicb  49520  funcoppc2  49612  uptpos  49667  prsthinc  49933  prstcle  50025  lanup  50110  ranup  50111  islmd  50134  cmddu  50137  lmdran  50140  cmdlan  50141