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

Theorem breq2i 4460
Description: Equality inference for a binary relation. (Contributed by NM, 8-Feb-1996.)
Hypothesis
Ref Expression
breq1i.1
Assertion
Ref Expression
breq2i

Proof of Theorem breq2i
StepHypRef Expression
1 breq1i.1 . 2
2 breq2 4456 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395   class class class wbr 4452
This theorem is referenced by:  breqtri  4475  en1  7602  snnen2o  7726  enp1i  7775  pm54.43  8402  addclprlem2  9416  map2psrpr  9508  lt0neg2  10084  le0neg2  10086  recgt1  10466  addltmul  10799  nn0lt10bOLD  10951  nn0lt2  10952  xlt0neg2  11448  xle0neg2  11450  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  hashen1  12439  swrdccatin2  12712  swrdccat3  12717  mertens  13695  aleph1re  13978  dvdslelem  14030  divalglem5  14055  ndvdsi  14068  bitsfzo  14085  3prm  14234  prmfac1  14259  dec2dvds  14549  dec5dvds2  14551  prmlem0  14591  dprd0  17078  ablfac1lem  17119  minveclem3b  21843  minveclem6  21849  minveclem7  21850  ioombl1lem4  21971  sinhalfpilem  22856  sincosq1lem  22890  sincosq1sgn  22891  sincosq2sgn  22892  sincosq3sgn  22893  sincosq4sgn  22894  bposlem6  23564  avril1  25171  minvecolem5  25797  minvecolem6  25798  minvecolem7  25799  bcsiALT  26096  pjdifnormii  26601  cvexchi  27288  ballotlem4  28437  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  lincdifsn  33025  lindslinindsimp1  33058  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  bnj110  33916  dalem18  35405  dalem48  35444  cdlemblem  35517  cdleme7ga  35973  cdlemg27b  36422  frege72  37963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453
  Copyright terms: Public domain W3C validator