Theorem breqd 5158

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   class class class wbr 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-br 5148

This theorem is referenced by:  breq123d  5161  breqdi  5162  sbcbr123  5201  sbcbr  5202  sbcbr12g  5203  fvmptopab  7486  fvmptopabOLD  7487  brfvopab  7489  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabovd  8105  mptmpoopabbrdOLDOLD  8106  mptmpoopabovdOLD  8107  bropopvvv  8113  bropfvvvvlem  8114  sprmpod  8247  fprlem1  8323  wfrlem5OLD  8351  supeq123d  9487  frrlem15  9794  fpwwe2lem11  10678  fpwwe2  10680  brtrclfv  15037  dfrtrclrec2  15093  rtrclreclem3  15095  relexpindlem  15098  shftfib  15107  2shfti  15115  prdsval  17501  pwsle  17538  pwsleval  17539  imasleval  17587  issect  17800  isinv  17807  brcic  17845  ciclcl  17849  cicrcl  17850  isfunc  17914  funcres2c  17954  isfull  17963  isfth  17967  fullpropd  17973  fthpropd  17974  elhoma  18085  isposd  18380  pltval  18389  lubfval  18407  glbfval  18420  joinfval  18430  meetfval  18444  odujoin  18465  odumeet  18467  ipole  18591  eqgval  19207  unitpropd  20433  rngcifuestrc  20655  znleval  21590  ltbval  22078  opsrval  22081  lmbr  23281  metustexhalf  24584  metucn  24599  isphtpc  25039  taylthlem1  26429  ulmval  26437  tgjustf  28495  iscgrg  28534  legov  28607  ishlg  28624  opphllem5  28773  opphllem6  28774  hpgbr  28782  iscgra  28831  acopy  28855  isinag  28860  isleag  28869  iseqlg  28889  wlkonprop  29690  wksonproplem  29736  wksonproplemOLD  29737  istrlson  29739  upgrwlkdvspth  29771  ispthson  29774  isspthson  29775  cyclispthon  29833  wspthsn  29877  wspthsnon  29881  iswspthsnon  29885  1pthon2v  30181  3wlkond  30199  dfconngr1  30216  isconngr  30217  isconngr1  30218  1conngr  30222  conngrv2edg  30223  minvecolem4b  30906  minvecolem4  30908  br8d  32629  ressprs  32938  resstos  32941  mntoval  32956  mgcoval  32960  mgcval  32961  isomnd  33060  submomnd  33069  ogrpaddltrd  33078  isinftm  33170  isorng  33308  rprmval  33523  metidv  33852  pstmfval  33856  faeval  34226  brfae  34228  isacycgr  35129  isacycgr1  35130  issconn  35210  satfbrsuc  35350  mclsax  35553  weiunpo  36447  weiunfr  36449  bj-imdirval3  37166  unceq  37583  alrmomodm  38340  relbrcoss  38427  lcvbr  39002  isopos  39161  cmtvalN  39192  isoml  39219  cvrfval  39249  cvrval  39250  pats  39266  isatl  39280  iscvlat  39304  ishlat1  39333  llnset  39487  lplnset  39511  lvolset  39554  lineset  39720  psubspset  39726  pmapfval  39738  lautset  40064  ldilfset  40090  ltrnfset  40099  trlfset  40142  diaffval  41012  dicffval  41156  dihffval  41212  prjspnvs  42606  fnwe2lem2  43039  fnwe2lem3  43040  aomclem8  43049  brfvid  43676  brfvidRP  43677  brfvrcld  43680  brfvrcld2  43681  iunrelexpuztr  43708  brtrclfv2  43716  neicvgnvor  44105  neicvgel1  44108  fperdvper  45874  upwlkbprop  47981  isprsd  48751  lubeldm2d  48754  glbeldm2d  48755  catprsc  48801  catprsc2  48802  prsthinc  48854  prstcle  48870