Theorem elprnq 10852

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2106  Qcnq 10713  Pcnp 10720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1089  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rex 3072  df-v 3444  df-in 3908  df-ss 3918  df-pss 3920  df-np 10842

This theorem is referenced by:  prub  10855  genpv  10860  genpdm  10863  genpss  10865  genpnnp  10866  genpnmax  10868  addclprlem1  10877  addclprlem2  10878  mulclprlem  10880  distrlem4pr  10887  1idpr  10890  psslinpr  10892  prlem934  10894  ltaddpr  10895  ltexprlem2  10898  ltexprlem3  10899  ltexprlem6  10902  ltexprlem7  10903  prlem936  10908  reclem2pr  10909  reclem3pr  10910  reclem4pr  10911