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

Theorem elprnq 9692
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 9691 . . 3 (𝐴P𝐴Q)
21pssssd 3666 . 2 (𝐴P𝐴Q)
32sselda 3568 1 ((𝐴P𝐵𝐴) → 𝐵Q)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 1977  Qcnq 9553  Pcnp 9560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-pss 3556  df-np 9682
This theorem is referenced by:  prub  9695  genpv  9700  genpdm  9703  genpss  9705  genpnnp  9706  genpnmax  9708  addclprlem1  9717  addclprlem2  9718  mulclprlem  9720  distrlem4pr  9727  1idpr  9730  psslinpr  9732  prlem934  9734  ltaddpr  9735  ltexprlem2  9738  ltexprlem3  9739  ltexprlem6  9742  ltexprlem7  9743  prlem936  9748  reclem2pr  9749  reclem3pr  9750  reclem4pr  9751
  Copyright terms: Public domain W3C validator