Theorem elprnq 10902

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  Qcnq 10763  Pcnp 10770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-v 3442  df-ss 3918  df-pss 3921  df-np 10892

This theorem is referenced by:  prub  10905  genpv  10910  genpdm  10913  genpss  10915  genpnnp  10916  genpnmax  10918  addclprlem1  10927  addclprlem2  10928  mulclprlem  10930  distrlem4pr  10937  1idpr  10940  psslinpr  10942  prlem934  10944  ltaddpr  10945  ltexprlem2  10948  ltexprlem3  10949  ltexprlem6  10952  ltexprlem7  10953  prlem936  10958  reclem2pr  10959  reclem3pr  10960  reclem4pr  10961