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

Theorem breq2i 4222
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 4218 . 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 178    = wceq 1653   class class class wbr 4214
This theorem is referenced by:  breqtri  4237  en1  7176  enp1i  7345  pm54.43  7889  addclprlem2  8896  map2psrpr  8987  lt0neg2  9537  le0neg2  9539  recgt1  9908  addltmul  10205  nn0lt10b  10338  xlt0neg2  10808  xle0neg2  10810  iccshftr  11032  iccshftl  11034  iccdil  11036  icccntr  11038  mertens  12665  aleph1re  12846  dvdslelem  12896  divalglem5  12919  ndvdsi  12932  bitsfzo  12949  3prm  13098  prmfac1  13120  dec2dvds  13401  dec5dvds2  13403  prmlem0  13430  dprd0  15591  ablfac1lem  15628  minveclem3b  19331  minveclem6  19337  minveclem7  19338  ioombl1lem4  19457  sinhalfpilem  20376  sincosq1lem  20407  sincosq1sgn  20408  sincosq2sgn  20409  sincosq3sgn  20410  sincosq4sgn  20411  bposlem6  21075  avril1  21759  minvecolem5  22385  minvecolem6  22386  minvecolem7  22387  bcsiALT  22683  pjdifnormii  23187  cvexchi  23874  ballotlem4  24758  jm2.23  27069  swrdccatin2  28212  swrdccat3  28217  bnj110  29231  dalem18  30480  dalem48  30519  cdlemblem  30592  cdleme7ga  31047  cdlemg27b  31495
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-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4215
  Copyright terms: Public domain W3C validator