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

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

Proof of Theorem breq1i
StepHypRef Expression
1 breq1i.1 . 2
2 breq1 4455 . 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:  eqbrtri  4471  brtpos0  6981  brtpos  6983  euen1  7605  euen1b  7606  2dom  7608  0sdom1dom  7737  modom2  7741  1sdom  7742  cnfcom3lem  8168  cnfcom3lemOLD  8176  pr2nelem  8403  axdclem2  8921  cfpwsdom  8980  inar1  9174  reclem3pr  9448  gt0srpr  9476  mappsrpr  9506  ltpsrpr  9507  map2psrpr  9508  axpre-mulgt0  9566  lt0neg1  10083  le0neg1  10085  reclt1  10465  addltmul  10799  uzindOLD  10982  eluz2b1  11182  xlt0neg1  11447  xle0neg1  11449  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  elfznelfzo  11915  bernneq  12292  nn0opthlem1  12348  faclbnd4lem1  12371  hashge0  12455  hashle00  12465  cbvsum  13517  cbvprod  13722  iprodmul  13796  divalglem1  14052  divalglem6  14056  isprm2lem  14224  isprm3  14226  isnzr2  17911  chrdvds  18565  chrcong  18566  lindsmm  18863  cpmidpmat  19374  csdfil  20395  iscau3  21717  ioombl1lem4  21971  itg2cn  22170  radcnvlt1  22813  sincosq1sgn  22891  sincosq3sgn  22893  sincosq4sgn  22894  ang180lem3  23143  leibpilem2  23272  issqf  23410  bposlem6  23564  clwlkisclwwlklem1  24787  frgra3v  25002  3vfriswmgra  25005  numclwwlkovf2ex  25086  cvexchi  27288  addltmulALT  27365  rnct  27539  dya2iocct  28251  ballotlemi1  28441  signswch  28518  divcnvshft  29117  wsuclb  29384  cos2h  30046  tan2h  30047  hashnzfzclim  31227  dvradcnv2  31252  binomcxplemnotnn0  31261  fourierdlem112  32001  lhpocnel2  35743  cdlemk19w  36698
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