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

Theorem ltrelnq 9207
 Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.) (New usage is discouraged.)
Assertion
Ref Expression
ltrelnq

Proof of Theorem ltrelnq
StepHypRef Expression
1 df-ltnq 9199 . 2
2 inss2 3680 . 2
31, 2eqsstri 3495 1
 Colors of variables: wff setvar class Syntax hints:   cin 3436   wss 3437   cxp 4947   cltpq 9129  cnq 9131   cltq 9137 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-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-v 3080  df-in 3444  df-ss 3451  df-ltnq 9199 This theorem is referenced by:  lterpq  9251  ltanq  9252  ltmnq  9253  ltexnq  9256  ltbtwnnq  9259  ltrnq  9260  prcdnq  9274  prnmadd  9278  genpcd  9287  nqpr  9295  1idpr  9310  prlem934  9314  ltexprlem4  9320  prlem936  9328  reclem2pr  9329  reclem3pr  9330  reclem4pr  9331
 Copyright terms: Public domain W3C validator