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

Theorem elprnq 8631
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  |-  ( ( A  e.  P.  /\  B  e.  A )  ->  B  e.  Q. )

Proof of Theorem elprnq
StepHypRef Expression
1 prpssnq 8630 . . 3  |-  ( A  e.  P.  ->  A  C.  Q. )
21pssssd 3286 . 2  |-  ( A  e.  P.  ->  A  C_ 
Q. )
32sselda 3193 1  |-  ( ( A  e.  P.  /\  B  e.  A )  ->  B  e.  Q. )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   Q.cnq 8490   P.cnp 8497
This theorem is referenced by:  prub  8634  genpv  8639  genpdm  8642  genpss  8644  genpnnp  8645  genpnmax  8647  addclprlem1  8656  addclprlem2  8657  mulclprlem  8659  distrlem4pr  8666  1idpr  8669  psslinpr  8671  prlem934  8673  ltaddpr  8674  ltexprlem2  8677  ltexprlem3  8678  ltexprlem6  8681  ltexprlem7  8682  prlem936  8687  reclem2pr  8688  reclem3pr  8689  reclem4pr  8690
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-v 2803  df-in 3172  df-ss 3179  df-pss 3181  df-np 8621
  Copyright terms: Public domain W3C validator