Theorem elprnq 10904

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Qcnq 10765  Pcnp 10772

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 3440  df-ss 3922  df-pss 3925  df-np 10894

This theorem is referenced by:  prub  10907  genpv  10912  genpdm  10915  genpss  10917  genpnnp  10918  genpnmax  10920  addclprlem1  10929  addclprlem2  10930  mulclprlem  10932  distrlem4pr  10939  1idpr  10942  psslinpr  10944  prlem934  10946  ltaddpr  10947  ltexprlem2  10950  ltexprlem3  10951  ltexprlem6  10954  ltexprlem7  10955  prlem936  10960  reclem2pr  10961  reclem3pr  10962  reclem4pr  10963