Theorem elprnq 11010

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  Qcnq 10871  Pcnp 10878

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-v 3466  df-ss 3948  df-pss 3951  df-np 11000

This theorem is referenced by:  prub  11013  genpv  11018  genpdm  11021  genpss  11023  genpnnp  11024  genpnmax  11026  addclprlem1  11035  addclprlem2  11036  mulclprlem  11038  distrlem4pr  11045  1idpr  11048  psslinpr  11050  prlem934  11052  ltaddpr  11053  ltexprlem2  11056  ltexprlem3  11057  ltexprlem6  11060  ltexprlem7  11061  prlem936  11066  reclem2pr  11067  reclem3pr  11068  reclem4pr  11069