Theorem elprnq 11032

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  Qcnq 10893  Pcnp 10900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-v 3481  df-ss 3967  df-pss 3970  df-np 11022

This theorem is referenced by:  prub  11035  genpv  11040  genpdm  11043  genpss  11045  genpnnp  11046  genpnmax  11048  addclprlem1  11057  addclprlem2  11058  mulclprlem  11060  distrlem4pr  11067  1idpr  11070  psslinpr  11072  prlem934  11074  ltaddpr  11075  ltexprlem2  11078  ltexprlem3  11079  ltexprlem6  11082  ltexprlem7  11083  prlem936  11088  reclem2pr  11089  reclem3pr  11090  reclem4pr  11091