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

Theorem breqi 4458
 Description: Equality inference for binary relations. (Contributed by NM, 19-Feb-2005.)
Hypothesis
Ref Expression
breqi.1
Assertion
Ref Expression
breqi

Proof of Theorem breqi
StepHypRef Expression
1 breqi.1 . 2
2 breq 4454 . 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:  f1ompt  6053  isocnv3  6228  brtpos2  6980  brwitnlem  7176  brdifun  7357  omxpenlem  7638  infxpenlem  8412  ltpiord  9286  nqerf  9329  nqerid  9332  ordpinq  9342  ltxrlt  9676  ltxr  11353  oduleg  15762  oduposb  15766  meet0  15767  join0  15768  xmeterval  20935  pi1cpbl  21544  ltgov  23983  brbtwn  24202  rgraprop  24928  rusgraprop  24929  rusgrargra  24930  avril1  25171  axhcompl-zf  25915  hlimadd  26110  hhcmpl  26117  hhcms  26120  hlim0  26153  fcoinvbr  27461  posrasymb  27645  trleile  27654  isarchi  27726  pstmfval  27875  pstmxmet  27876  lmlim  27929  brtxp  29530  brpprod  29535  brpprod3b  29537  brtxpsd2  29545  brdomain  29583  brrange  29584  brimg  29587  brapply  29588  brsuccf  29591  brrestrict  29599  brub  29604  brlb  29605  colineardim1  29711  broutsideof  29771  fneval  30170  climreeq  31619  gte-lte  33118  gt-lt  33119  gte-lteh  33120  gt-lth  33121  trclubg  37785 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-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452  df-br 4453
 Copyright terms: Public domain W3C validator