Theorem breqd 5134

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   class class class wbr 5123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-clel 2808  df-br 5124

This theorem is referenced by:  breq123d  5137  breqdi  5138  sbcbr123  5177  sbcbr  5178  sbcbr12g  5179  fvmptopab  7469  fvmptopabOLD  7470  brfvopab  7472  mptmpoopabbrd  8087  mptmpoopabbrdOLD  8088  mptmpoopabovd  8089  mptmpoopabbrdOLDOLD  8090  mptmpoopabovdOLD  8091  bropopvvv  8097  bropfvvvvlem  8098  sprmpod  8231  fprlem1  8307  wfrlem5OLD  8335  supeq123d  9472  frrlem15  9779  fpwwe2lem11  10663  fpwwe2  10665  brtrclfv  15023  dfrtrclrec2  15079  rtrclreclem3  15081  relexpindlem  15084  shftfib  15093  2shfti  15101  prdsval  17471  pwsle  17508  pwsleval  17509  imasleval  17557  issect  17768  isinv  17775  brcic  17813  ciclcl  17817  cicrcl  17818  isfunc  17880  funcres2c  17919  isfull  17928  isfth  17932  fullpropd  17938  fthpropd  17939  elhoma  18048  isposd  18338  pltval  18346  lubfval  18364  glbfval  18377  joinfval  18387  meetfval  18401  odujoin  18422  odumeet  18424  ipole  18548  eqgval  19164  unitpropd  20385  rngcifuestrc  20607  znleval  21527  ltbval  22015  opsrval  22018  lmbr  23212  metustexhalf  24513  metucn  24528  isphtpc  24962  taylthlem1  26351  ulmval  26359  tgjustf  28417  iscgrg  28456  legov  28529  ishlg  28546  opphllem5  28695  opphllem6  28696  hpgbr  28704  iscgra  28753  acopy  28777  isinag  28782  isleag  28791  iseqlg  28811  wlkonprop  29604  wksonproplem  29650  wksonproplemOLD  29651  istrlson  29653  upgrwlkdvspth  29687  ispthson  29690  isspthson  29691  cyclispthon  29752  wspthsn  29796  wspthsnon  29800  iswspthsnon  29804  1pthon2v  30100  3wlkond  30118  dfconngr1  30135  isconngr  30136  isconngr1  30137  1conngr  30141  conngrv2edg  30142  minvecolem4b  30825  minvecolem4  30827  br8d  32557  ressprs  32893  resstos  32896  mntoval  32911  mgcoval  32915  mgcval  32916  isomnd  33017  submomnd  33026  ogrpaddltrd  33035  isinftm  33127  isorng  33269  rprmval  33479  metidv  33850  pstmfval  33854  faeval  34206  brfae  34208  isacycgr  35109  isacycgr1  35110  issconn  35190  satfbrsuc  35330  mclsax  35533  weiunpo  36425  weiunfr  36427  bj-imdirval3  37144  unceq  37563  alrmomodm  38319  relbrcoss  38406  lcvbr  38981  isopos  39140  cmtvalN  39171  isoml  39198  cvrfval  39228  cvrval  39229  pats  39245  isatl  39259  iscvlat  39283  ishlat1  39312  llnset  39466  lplnset  39490  lvolset  39533  lineset  39699  psubspset  39705  pmapfval  39717  lautset  40043  ldilfset  40069  ltrnfset  40078  trlfset  40121  diaffval  40991  dicffval  41135  dihffval  41191  prjspnvs  42593  fnwe2lem2  43026  fnwe2lem3  43027  aomclem8  43036  brfvid  43662  brfvidRP  43663  brfvrcld  43666  brfvrcld2  43667  iunrelexpuztr  43694  brtrclfv2  43702  neicvgnvor  44091  neicvgel1  44094  fperdvper  45891  upwlkbprop  48012  isprsd  48812  lubeldm2d  48815  glbeldm2d  48816  catprsc  48870  catprsc2  48871  prsthinc  49089  prstcle  49160