Theorem elprnq 10944

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-v 3449  df-ss 3931  df-pss 3934  df-np 10934

This theorem is referenced by:  prub  10947  genpv  10952  genpdm  10955  genpss  10957  genpnnp  10958  genpnmax  10960  addclprlem1  10969  addclprlem2  10970  mulclprlem  10972  distrlem4pr  10979  1idpr  10982  psslinpr  10984  prlem934  10986  ltaddpr  10987  ltexprlem2  10990  ltexprlem3  10991  ltexprlem6  10994  ltexprlem7  10995  prlem936  11000  reclem2pr  11001  reclem3pr  11002  reclem4pr  11003