Theorem elprnq 11060

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  Qcnq 10921  Pcnp 10928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-v 3490  df-ss 3993  df-pss 3996  df-np 11050

This theorem is referenced by:  prub  11063  genpv  11068  genpdm  11071  genpss  11073  genpnnp  11074  genpnmax  11076  addclprlem1  11085  addclprlem2  11086  mulclprlem  11088  distrlem4pr  11095  1idpr  11098  psslinpr  11100  prlem934  11102  ltaddpr  11103  ltexprlem2  11106  ltexprlem3  11107  ltexprlem6  11110  ltexprlem7  11111  prlem936  11116  reclem2pr  11117  reclem3pr  11118  reclem4pr  11119