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

Theorem elprnq 10934
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 10933 . . 3 (𝐴P𝐴Q)
21pssssd 4062 . 2 (𝐴P𝐴Q)
32sselda 3949 1 ((𝐴P𝐵𝐴) → 𝐵Q)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107  Qcnq 10795  Pcnp 10802
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-v 3450  df-in 3922  df-ss 3932  df-pss 3934  df-np 10924
This theorem is referenced by:  prub  10937  genpv  10942  genpdm  10945  genpss  10947  genpnnp  10948  genpnmax  10950  addclprlem1  10959  addclprlem2  10960  mulclprlem  10962  distrlem4pr  10969  1idpr  10972  psslinpr  10974  prlem934  10976  ltaddpr  10977  ltexprlem2  10980  ltexprlem3  10981  ltexprlem6  10984  ltexprlem7  10985  prlem936  10990  reclem2pr  10991  reclem3pr  10992  reclem4pr  10993
  Copyright terms: Public domain W3C validator