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

Theorem elprnq 9390
 Description: A positive real is a set of positive fractions. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
Assertion
Ref Expression
elprnq

Proof of Theorem elprnq
StepHypRef Expression
1 prpssnq 9389 . . 3
21pssssd 3600 . 2
32sselda 3503 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   cnq 9251   cnp 9258 This theorem is referenced by:  prub  9393  genpv  9398  genpdm  9401  genpss  9403  genpnnp  9404  genpnmax  9406  addclprlem1  9415  addclprlem2  9416  mulclprlem  9418  distrlem4pr  9425  1idpr  9428  psslinpr  9430  prlem934  9432  ltaddpr  9433  ltexprlem2  9436  ltexprlem3  9437  ltexprlem6  9440  ltexprlem7  9441  prlem936  9446  reclem2pr  9447  reclem3pr  9448  reclem4pr  9449 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-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-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-pss 3491  df-np 9380
 Copyright terms: Public domain W3C validator