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

Theorem elprnq 10404
 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 10403 . . 3 (𝐴P𝐴Q)
21pssssd 4025 . 2 (𝐴P𝐴Q)
32sselda 3915 1 ((𝐴P𝐵𝐴) → 𝐵Q)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  Qcnq 10265  Pcnp 10272 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-in 3888  df-ss 3898  df-pss 3900  df-np 10394 This theorem is referenced by:  prub  10407  genpv  10412  genpdm  10415  genpss  10417  genpnnp  10418  genpnmax  10420  addclprlem1  10429  addclprlem2  10430  mulclprlem  10432  distrlem4pr  10439  1idpr  10442  psslinpr  10444  prlem934  10446  ltaddpr  10447  ltexprlem2  10450  ltexprlem3  10451  ltexprlem6  10454  ltexprlem7  10455  prlem936  10460  reclem2pr  10461  reclem3pr  10462  reclem4pr  10463
 Copyright terms: Public domain W3C validator