MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  breqd Unicode version

Theorem breqd 4034
Description: Equality deduction for a binary relation. (Contributed by NM, 29-Oct-2011.)
Hypothesis
Ref Expression
breq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
breqd  |-  ( ph  ->  ( C A D  <-> 
C B D ) )

Proof of Theorem breqd
StepHypRef Expression
1 breq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 breq 4025 . 2  |-  ( A  =  B  ->  ( C A D  <->  C B D ) )
31, 2syl 15 1  |-  ( ph  ->  ( C A D  <-> 
C B D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  breq123d  4037  sbcbr12g  4073  fpwwe2lem12  8263  fpwwe2  8265  shftfib  11567  2shfti  11575  prdsval  13355  pwsle  13391  pwsleval  13392  imasleval  13443  issect  13656  isinv  13662  episect  13683  isfunc  13738  funcres2c  13775  isfull  13784  isfth  13788  fullpropd  13794  fthpropd  13795  elhoma  13864  isposd  14089  pltval  14094  lubfval  14112  glbfval  14117  ipole  14261  eqgval  14666  unitpropd  15479  ltbval  16213  opsrval  16216  znleval  16508  lmbr  16988  isphtpc  18492  dvef  19327  taylthlem1  19752  ulmval  19759  minvecolem4b  21457  minvecolem4  21459  isscon  23757  iseupa  23881  relexpindlem  24036  dfrtrclrec2  24040  rtrclreclem.trans  24043  wfrlem5  24260  frrlem5  24285  isorhom  25211  isoriso  25212  isside1  26165  bosser  26167  fnwe2lem2  27148  fnwe2lem3  27149  supeq123d  27158  aomclem8  27159  lcvbr  29211  isopos  29370  cmtvalN  29401  isoml  29428  cvrfval  29458  cvrval  29459  pats  29475  isatl  29489  iscvlat  29513  ishlat1  29542  llnset  29694  lplnset  29718  lvolset  29761  lineset  29927  psubspset  29933  pmapfval  29945  lautset  30271  ldilfset  30297  ltrnfset  30306  trlfset  30349  diaffval  31220  dicffval  31364  dihffval  31420
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279  df-br 4024
  Copyright terms: Public domain W3C validator