Theorem elprnq 10912

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  Qcnq 10773  Pcnp 10780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rex 3065  df-v 3434  df-ss 3907  df-pss 3910  df-np 10902

This theorem is referenced by:  prub  10915  genpv  10920  genpdm  10923  genpss  10925  genpnnp  10926  genpnmax  10928  addclprlem1  10937  addclprlem2  10938  mulclprlem  10940  distrlem4pr  10947  1idpr  10950  psslinpr  10952  prlem934  10954  ltaddpr  10955  ltexprlem2  10958  ltexprlem3  10959  ltexprlem6  10962  ltexprlem7  10963  prlem936  10968  reclem2pr  10969  reclem3pr  10970  reclem4pr  10971