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

Theorem ltrelsr 9353
 Description: Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
Assertion
Ref Expression
ltrelsr

Proof of Theorem ltrelsr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ltr 9345 . 2
2 opabssxp 5022 . 2
31, 2eqsstri 3497 1
 Colors of variables: wff setvar class Syntax hints:   wa 369   wceq 1370  wex 1587   wcel 1758   wss 3439  cop 3994   class class class wbr 4403  copab 4460   cxp 4949  (class class class)co 6203  cec 7212   cpp 9143   cltp 9145   cer 9148  cnr 9149   cltr 9155 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 1955  ax-ext 2432 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3446  df-ss 3453  df-opab 4462  df-xp 4957  df-ltr 9345 This theorem is referenced by:  ltsrpr  9359  ltasr  9382  recexsrlem  9385  addgt0sr  9386  mulgt0sr  9387  map2psrpr  9392  supsrlem  9393  supsr  9394  ltresr  9422  axpre-lttrn  9448
 Copyright terms: Public domain W3C validator