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

Theorem breq2i 4401
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 4397 . 2  |-  ( A  =  B  ->  ( C R A  <->  C R B ) )
31, 2ax-mp 5 1  |-  ( C R A  <->  C R B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1370   class class class wbr 4393
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-br 4394
This theorem is referenced by:  breqtri  4416  en1  7479  snnen2o  7603  enp1i  7651  pm54.43  8274  addclprlem2  9290  map2psrpr  9381  lt0neg2  9950  le0neg2  9952  recgt1  10332  addltmul  10664  nn0lt10b  10810  xlt0neg2  11294  xle0neg2  11296  iccshftr  11529  iccshftl  11531  iccdil  11533  icccntr  11535  hashen1  12247  swrdccatin2  12489  swrdccat3  12494  mertens  13457  aleph1re  13638  dvdslelem  13688  divalglem5  13712  ndvdsi  13725  bitsfzo  13742  3prm  13891  prmfac1  13915  dec2dvds  14203  dec5dvds2  14205  prmlem0  14244  dprd0  16642  ablfac1lem  16683  minveclem3b  21040  minveclem6  21046  minveclem7  21047  ioombl1lem4  21168  sinhalfpilem  22051  sincosq1lem  22085  sincosq1sgn  22086  sincosq2sgn  22087  sincosq3sgn  22088  sincosq4sgn  22089  bposlem6  22754  avril1  23801  minvecolem5  24427  minvecolem6  24428  minvecolem7  24429  bcsiALT  24726  pjdifnormii  25231  cvexchi  25918  gsumle  26384  ballotlem4  27018  nn0lt2  30327  lincdifsn  31068  lindslinindsimp1  31101  lindslinindsimp2lem5  31106  lindslinindsimp2  31107  bnj110  32154  dalem18  33634  dalem48  33673  cdlemblem  33746  cdleme7ga  34201  cdlemg27b  34649
  Copyright terms: Public domain W3C validator