Theorem elprnq 10747

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  Qcnq 10608  Pcnp 10615

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ne 2944  df-ral 3069  df-rex 3070  df-v 3434  df-in 3894  df-ss 3904  df-pss 3906  df-np 10737

This theorem is referenced by:  prub  10750  genpv  10755  genpdm  10758  genpss  10760  genpnnp  10761  genpnmax  10763  addclprlem1  10772  addclprlem2  10773  mulclprlem  10775  distrlem4pr  10782  1idpr  10785  psslinpr  10787  prlem934  10789  ltaddpr  10790  ltexprlem2  10793  ltexprlem3  10794  ltexprlem6  10797  ltexprlem7  10798  prlem936  10803  reclem2pr  10804  reclem3pr  10805  reclem4pr  10806