Theorem breqd 5110

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

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

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 5100

This theorem is referenced by:  breq123d  5113  breqdi  5114  sbcbr123  5153  sbcbr  5154  sbcbr12g  5155  fvmptopab  7416  brfvopab  7418  mptmpoopabbrd  8027  mptmpoopabbrdOLD  8028  mptmpoopabovd  8029  bropopvvv  8035  bropfvvvvlem  8036  sprmpod  8169  fprlem1  8245  supeq123d  9358  frrlem15  9674  fpwwe2lem11  10557  fpwwe2  10559  brtrclfv  14930  dfrtrclrec2  14986  rtrclreclem3  14988  relexpindlem  14991  shftfib  15000  2shfti  15008  prdsval  17380  pwsle  17418  pwsleval  17419  imasleval  17467  issect  17682  isinv  17689  brcic  17727  ciclcl  17731  cicrcl  17732  isfunc  17793  funcres2c  17832  isfull  17841  isfth  17845  fullpropd  17851  fthpropd  17852  elhoma  17961  isposd  18250  pltval  18258  lubfval  18276  glbfval  18289  joinfval  18299  meetfval  18313  odujoin  18334  odumeet  18336  resstos  18358  ipole  18462  eqgval  19111  isomnd  20057  submomnd  20066  ogrpaddltrd  20074  unitpropd  20358  rngcifuestrc  20577  isorng  20799  znleval  21514  ltbval  22003  opsrval  22006  lmbr  23207  metustexhalf  24505  metucn  24520  isphtpc  24954  taylthlem1  26342  ulmval  26350  tgjustf  28550  iscgrg  28589  legov  28662  ishlg  28679  opphllem5  28828  opphllem6  28829  hpgbr  28837  iscgra  28886  acopy  28910  isinag  28915  isleag  28924  iseqlg  28944  wlkonprop  29735  wksonproplem  29781  istrlson  29783  upgrwlkdvspth  29817  ispthson  29820  isspthson  29821  cyclispthon  29882  wspthsn  29926  wspthsnon  29930  iswspthsnon  29934  1pthon2v  30233  3wlkond  30251  dfconngr1  30268  isconngr  30269  isconngr1  30270  1conngr  30274  conngrv2edg  30275  minvecolem4b  30958  minvecolem4  30960  br8d  32690  ressprs  33051  mntoval  33067  mgcoval  33071  mgcval  33072  isinftm  33267  rprmval  33601  metidv  34062  pstmfval  34066  faeval  34416  brfae  34418  isacycgr  35352  isacycgr1  35353  issconn  35433  satfbrsuc  35573  mclsax  35776  weiunpo  36672  weiunfr  36674  bj-imdirval3  37402  unceq  37811  alrmomodm  38573  relbrcoss  38750  lcvbr  39360  isopos  39519  cmtvalN  39550  isoml  39577  cvrfval  39607  cvrval  39608  pats  39624  isatl  39638  iscvlat  39662  ishlat1  39691  llnset  39844  lplnset  39868  lvolset  39911  lineset  40077  psubspset  40083  pmapfval  40095  lautset  40421  ldilfset  40447  ltrnfset  40456  trlfset  40499  diaffval  41369  dicffval  41513  dihffval  41569  prjspnvs  42941  fnwe2lem2  43371  fnwe2lem3  43372  aomclem8  43381  brfvid  44006  brfvidRP  44007  brfvrcld  44010  brfvrcld2  44011  iunrelexpuztr  44038  brtrclfv2  44046  neicvgnvor  44435  neicvgel1  44438  fperdvper  46240  upwlkbprop  48461  isprsd  49277  lubeldm2d  49280  glbeldm2d  49281  catprsc  49335  catprsc2  49336  oppccicb  49373  funcoppc2  49465  uptpos  49520  prsthinc  49786  prstcle  49878  lanup  49963  ranup  49964  islmd  49987  cmddu  49990  lmdran  49993  cmdlan  49994