Theorem elprnq 10605

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  Qcnq 10466  Pcnp 10473

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3066  df-rex 3067  df-v 3410  df-in 3873  df-ss 3883  df-pss 3885  df-np 10595

This theorem is referenced by:  prub  10608  genpv  10613  genpdm  10616  genpss  10618  genpnnp  10619  genpnmax  10621  addclprlem1  10630  addclprlem2  10631  mulclprlem  10633  distrlem4pr  10640  1idpr  10643  psslinpr  10645  prlem934  10647  ltaddpr  10648  ltexprlem2  10651  ltexprlem3  10652  ltexprlem6  10655  ltexprlem7  10656  prlem936  10661  reclem2pr  10662  reclem3pr  10663  reclem4pr  10664