Theorem elprnq 10951

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 10950	. . 3 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q)
2	1	pssssd 4066	. 2 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q)
3	2	sselda 3949	1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ Q)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Qcnq 10812  Pcnp 10819

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-v 3452  df-ss 3934  df-pss 3937  df-np 10941

This theorem is referenced by:  prub  10954  genpv  10959  genpdm  10962  genpss  10964  genpnnp  10965  genpnmax  10967  addclprlem1  10976  addclprlem2  10977  mulclprlem  10979  distrlem4pr  10986  1idpr  10989  psslinpr  10991  prlem934  10993  ltaddpr  10994  ltexprlem2  10997  ltexprlem3  10998  ltexprlem6  11001  ltexprlem7  11002  prlem936  11007  reclem2pr  11008  reclem3pr  11009  reclem4pr  11010