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

Theorem breq2i 4047
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 4043 . 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 1632   class class class wbr 4039
This theorem is referenced by:  breqtri  4062  en1  6944  enp1i  7109  pm54.43  7649  addclprlem2  8657  map2psrpr  8748  lt0neg2  9297  le0neg2  9299  recgt1  9668  addltmul  9963  nn0lt10b  10094  xlt0neg2  10563  xle0neg2  10565  iccshftr  10785  iccshftl  10787  iccdil  10789  icccntr  10791  mertens  12358  aleph1re  12539  dvdslelem  12589  divalglem5  12612  ndvdsi  12625  bitsfzo  12642  3prm  12791  prmfac1  12813  dec2dvds  13094  dec5dvds2  13096  prmlem0  13123  dprd0  15282  ablfac1lem  15319  minveclem3b  18808  minveclem6  18814  minveclem7  18815  ioombl1lem4  18934  sinhalfpilem  19850  sincosq1lem  19881  sincosq1sgn  19882  sincosq2sgn  19883  sincosq3sgn  19884  sincosq4sgn  19885  bposlem6  20544  avril1  20852  minvecolem5  21476  minvecolem6  21477  minvecolem7  21478  bcsiALT  21774  pjdifnormii  22278  cvexchi  22965  ballotlem4  23073  ballotlem1c  23082  xrge0iifcnv  23330  jm2.23  27192  bnj110  29206  dalem18  30492  dalem48  30531  cdlemblem  30604  cdleme7ga  31059  cdlemg27b  31507
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-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-br 4040
  Copyright terms: Public domain W3C validator