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

Theorem breqd 4050
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 4041 . 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 1632   class class class wbr 4039
This theorem is referenced by:  breq123d  4053  sbcbr12g  4089  fpwwe2lem12  8279  fpwwe2  8281  shftfib  11583  2shfti  11591  prdsval  13371  pwsle  13407  pwsleval  13408  imasleval  13459  issect  13672  isinv  13678  episect  13699  isfunc  13754  funcres2c  13791  isfull  13800  isfth  13804  fullpropd  13810  fthpropd  13811  elhoma  13880  isposd  14105  pltval  14110  lubfval  14128  glbfval  14133  ipole  14277  eqgval  14682  unitpropd  15495  ltbval  16229  opsrval  16232  znleval  16524  lmbr  17004  isphtpc  18508  dvef  19343  taylthlem1  19768  ulmval  19775  minvecolem4b  21473  minvecolem4  21475  isscon  23772  iseupa  23896  relexpindlem  24051  dfrtrclrec2  24055  rtrclreclem.trans  24058  wfrlem5  24331  frrlem5  24356  isorhom  25314  isoriso  25315  isside1  26268  bosser  26270  fnwe2lem2  27251  fnwe2lem3  27252  supeq123d  27261  aomclem8  27262  sprmpt2  28207  iswlkon  28332  trls  28335  trlon  28339  istrlon  28340  trlonprop  28341  pths  28352  spths  28353  pthon  28361  ispthon  28362  cyclispthon  28378  lcvbr  29833  isopos  29992  cmtvalN  30023  isoml  30050  cvrfval  30080  cvrval  30081  pats  30097  isatl  30111  iscvlat  30135  ishlat1  30164  llnset  30316  lplnset  30340  lvolset  30383  lineset  30549  psubspset  30555  pmapfval  30567  lautset  30893  ldilfset  30919  ltrnfset  30928  trlfset  30971  diaffval  31842  dicffval  31986  dihffval  32042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292  df-br 4040
  Copyright terms: Public domain W3C validator