Theorem elprnq 10678

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Qcnq 10539  Pcnp 10546

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-v 3424  df-in 3890  df-ss 3900  df-pss 3902  df-np 10668

This theorem is referenced by:  prub  10681  genpv  10686  genpdm  10689  genpss  10691  genpnnp  10692  genpnmax  10694  addclprlem1  10703  addclprlem2  10704  mulclprlem  10706  distrlem4pr  10713  1idpr  10716  psslinpr  10718  prlem934  10720  ltaddpr  10721  ltexprlem2  10724  ltexprlem3  10725  ltexprlem6  10728  ltexprlem7  10729  prlem936  10734  reclem2pr  10735  reclem3pr  10736  reclem4pr  10737