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

Theorem breqd 4224
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 4215 . 2  |-  ( A  =  B  ->  ( C A D  <->  C B D ) )
31, 2syl 16 1  |-  ( ph  ->  ( C A D  <-> 
C B D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653   class class class wbr 4213
This theorem is referenced by:  breq123d  4227  sbcbr12g  4263  bropopvvv  6427  sprmpt2  6477  supeq123d  7456  fpwwe2lem12  8517  fpwwe2  8519  shftfib  11888  2shfti  11896  prdsval  13679  pwsle  13715  pwsleval  13716  imasleval  13767  issect  13980  isinv  13986  episect  14007  isfunc  14062  funcres2c  14099  isfull  14108  isfth  14112  fullpropd  14118  fthpropd  14119  elhoma  14188  isposd  14413  pltval  14418  lubfval  14436  glbfval  14441  ipole  14585  eqgval  14990  unitpropd  15803  ltbval  16533  opsrval  16536  znleval  16836  lmbr  17323  metustexhalfOLD  18594  metustexhalf  18595  metucnOLD  18619  metucn  18620  isphtpc  19020  dvef  19865  taylthlem1  20290  ulmval  20297  wlkon  21531  iswlkon  21532  wlkonprop  21533  trls  21537  trlon  21541  istrlon  21542  trlonprop  21543  pths  21567  spths  21568  pthon  21576  ispthon  21577  pthonprop  21578  spthon  21583  isspthon  21584  spthonprp  21586  cyclispthon  21621  dfconngra1  21659  isconngra  21660  isconngra1  21661  1conngra  21663  iseupa  21688  minvecolem4b  22381  minvecolem4  22383  resstos  24189  isofld  24236  subofld  24246  isinftm  24252  metidv  24288  pstmfval  24292  faeval  24598  brfae  24600  isscon  24914  relexpindlem  25140  dfrtrclrec2  25144  rtrclreclem.trans  25147  wfrlem5  25543  frrlem5  25587  fnwe2lem2  27127  fnwe2lem3  27128  aomclem8  27137  is2wlkonot  28331  is2spthonot  28332  2wlkonot  28333  2spthonot  28334  2wlkonot3v  28343  2spthonot3v  28344  lcvbr  29820  isopos  29979  cmtvalN  30010  isoml  30037  cvrfval  30067  cvrval  30068  pats  30084  isatl  30098  iscvlat  30122  ishlat1  30151  llnset  30303  lplnset  30327  lvolset  30370  lineset  30536  psubspset  30542  pmapfval  30554  lautset  30880  ldilfset  30906  ltrnfset  30915  trlfset  30958  diaffval  31829  dicffval  31973  dihffval  32029
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2418
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2430  df-clel 2433  df-br 4214
  Copyright terms: Public domain W3C validator