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

Theorem breq2i 4031
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1i.1  |-  A  =  B
Assertion
Ref Expression
breq2i  |-  ( C R A  <->  C R B )

Proof of Theorem breq2i
StepHypRef Expression
1 breq1i.1 . 2  |-  A  =  B
2 breq2 4027 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2ax-mp 8 1  |-  ( C R A  <->  C R B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623   class class class wbr 4023
This theorem is referenced by:  breqtri  4046  en1  6928  enp1i  7093  pm54.43  7633  addclprlem2  8641  map2psrpr  8732  lt0neg2  9281  le0neg2  9283  recgt1  9652  addltmul  9947  nn0lt10b  10078  xlt0neg2  10547  xle0neg2  10549  iccshftr  10769  iccshftl  10771  iccdil  10773  icccntr  10775  mertens  12342  aleph1re  12523  dvdslelem  12573  divalglem5  12596  ndvdsi  12609  bitsfzo  12626  3prm  12775  prmfac1  12797  dec2dvds  13078  dec5dvds2  13080  prmlem0  13107  dprd0  15266  ablfac1lem  15303  minveclem3b  18792  minveclem6  18798  minveclem7  18799  ioombl1lem4  18918  sinhalfpilem  19834  sincosq1lem  19865  sincosq1sgn  19866  sincosq2sgn  19867  sincosq3sgn  19868  sincosq4sgn  19869  bposlem6  20528  avril1  20836  minvecolem5  21460  minvecolem6  21461  minvecolem7  21462  bcsiALT  21758  pjdifnormii  22262  cvexchi  22949  ballotlem4  23057  ballotlem1c  23066  xrge0iifcnv  23315  jm2.23  27089  bnj110  28890  dalem18  29870  dalem48  29909  cdlemblem  29982  cdleme7ga  30437  cdlemg27b  30885
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-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024
  Copyright terms: Public domain W3C validator