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

Theorem elprnq 9757
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 ((𝐴P𝐵𝐴) → 𝐵Q)

Proof of Theorem elprnq
StepHypRef Expression
1 prpssnq 9756 . . 3 (𝐴P𝐴Q)
21pssssd 3682 . 2 (𝐴P𝐴Q)
32sselda 3583 1 ((𝐴P𝐵𝐴) → 𝐵Q)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wcel 1987  Qcnq 9618  Pcnp 9625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-v 3188  df-in 3562  df-ss 3569  df-pss 3571  df-np 9747
This theorem is referenced by:  prub  9760  genpv  9765  genpdm  9768  genpss  9770  genpnnp  9771  genpnmax  9773  addclprlem1  9782  addclprlem2  9783  mulclprlem  9785  distrlem4pr  9792  1idpr  9795  psslinpr  9797  prlem934  9799  ltaddpr  9800  ltexprlem2  9803  ltexprlem3  9804  ltexprlem6  9807  ltexprlem7  9808  prlem936  9813  reclem2pr  9814  reclem3pr  9815  reclem4pr  9816
  Copyright terms: Public domain W3C validator