Theorem elprnq 10889

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

Step	Hyp	Ref	Expression
1		prpssnq 10888	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q)
2	1	pssssd 4049	. 2 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q)
3	2	sselda 3930	1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ Q)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Qcnq 10750  Pcnp 10757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-v 3439  df-ss 3915  df-pss 3918  df-np 10879

This theorem is referenced by:  prub  10892  genpv  10897  genpdm  10900  genpss  10902  genpnnp  10903  genpnmax  10905  addclprlem1  10914  addclprlem2  10915  mulclprlem  10917  distrlem4pr  10924  1idpr  10927  psslinpr  10929  prlem934  10931  ltaddpr  10932  ltexprlem2  10935  ltexprlem3  10936  ltexprlem6  10939  ltexprlem7  10940  prlem936  10945  reclem2pr  10946  reclem3pr  10947  reclem4pr  10948