Theorem breqd 5108

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2727  df-clel 2810  df-br 5098

This theorem is referenced by:  breq123d  5111  breqdi  5112  sbcbr123  5151  sbcbr  5152  sbcbr12g  5153  fvmptopab  7413  brfvopab  7415  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  mptmpoopabovd  8026  bropopvvv  8032  bropfvvvvlem  8033  sprmpod  8166  fprlem1  8242  supeq123d  9355  frrlem15  9671  fpwwe2lem11  10554  fpwwe2  10556  brtrclfv  14927  dfrtrclrec2  14983  rtrclreclem3  14985  relexpindlem  14988  shftfib  14997  2shfti  15005  prdsval  17377  pwsle  17415  pwsleval  17416  imasleval  17464  issect  17679  isinv  17686  brcic  17724  ciclcl  17728  cicrcl  17729  isfunc  17790  funcres2c  17829  isfull  17838  isfth  17842  fullpropd  17848  fthpropd  17849  elhoma  17958  isposd  18247  pltval  18255  lubfval  18273  glbfval  18286  joinfval  18296  meetfval  18310  odujoin  18331  odumeet  18333  resstos  18355  ipole  18459  eqgval  19108  isomnd  20054  submomnd  20063  ogrpaddltrd  20071  unitpropd  20355  rngcifuestrc  20574  isorng  20796  znleval  21511  ltbval  22000  opsrval  22003  lmbr  23204  metustexhalf  24502  metucn  24517  isphtpc  24951  taylthlem1  26339  ulmval  26347  tgjustf  28526  iscgrg  28565  legov  28638  ishlg  28655  opphllem5  28804  opphllem6  28805  hpgbr  28813  iscgra  28862  acopy  28886  isinag  28891  isleag  28900  iseqlg  28920  wlkonprop  29711  wksonproplem  29757  istrlson  29759  upgrwlkdvspth  29793  ispthson  29796  isspthson  29797  cyclispthon  29858  wspthsn  29902  wspthsnon  29906  iswspthsnon  29910  1pthon2v  30209  3wlkond  30227  dfconngr1  30244  isconngr  30245  isconngr1  30246  1conngr  30250  conngrv2edg  30251  minvecolem4b  30934  minvecolem4  30936  br8d  32666  ressprs  33027  mntoval  33043  mgcoval  33047  mgcval  33048  isinftm  33242  rprmval  33576  metidv  34028  pstmfval  34032  faeval  34382  brfae  34384  isacycgr  35318  isacycgr1  35319  issconn  35399  satfbrsuc  35539  mclsax  35742  weiunpo  36638  weiunfr  36640  bj-imdirval3  37358  unceq  37767  alrmomodm  38529  relbrcoss  38706  lcvbr  39316  isopos  39475  cmtvalN  39506  isoml  39533  cvrfval  39563  cvrval  39564  pats  39580  isatl  39594  iscvlat  39618  ishlat1  39647  llnset  39800  lplnset  39824  lvolset  39867  lineset  40033  psubspset  40039  pmapfval  40051  lautset  40377  ldilfset  40403  ltrnfset  40412  trlfset  40455  diaffval  41325  dicffval  41469  dihffval  41525  prjspnvs  42900  fnwe2lem2  43330  fnwe2lem3  43331  aomclem8  43340  brfvid  43965  brfvidRP  43966  brfvrcld  43969  brfvrcld2  43970  iunrelexpuztr  43997  brtrclfv2  44005  neicvgnvor  44394  neicvgel1  44397  fperdvper  46200  upwlkbprop  48421  isprsd  49237  lubeldm2d  49240  glbeldm2d  49241  catprsc  49295  catprsc2  49296  oppccicb  49333  funcoppc2  49425  uptpos  49480  prsthinc  49746  prstcle  49838  lanup  49923  ranup  49924  islmd  49947  cmddu  49950  lmdran  49953  cmdlan  49954