Theorem elprnq 10988

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

Syntax hints:   → wi 4   ∧ wa 394   ∈ wcel 2104  Qcnq 10849  Pcnp 10856

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1087  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-v 3474  df-in 3954  df-ss 3964  df-pss 3966  df-np 10978

This theorem is referenced by:  prub  10991  genpv  10996  genpdm  10999  genpss  11001  genpnnp  11002  genpnmax  11004  addclprlem1  11013  addclprlem2  11014  mulclprlem  11016  distrlem4pr  11023  1idpr  11026  psslinpr  11028  prlem934  11030  ltaddpr  11031  ltexprlem2  11034  ltexprlem3  11035  ltexprlem6  11038  ltexprlem7  11039  prlem936  11044  reclem2pr  11045  reclem3pr  11046  reclem4pr  11047