Theorem elprnq 11079

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  Qcnq 10940  Pcnp 10947

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-v 3452  df-ss 3896  df-pss 4014  df-np 11069

This theorem is used by:  prub  11082  genpv  11087  genpdm  11090  genpss  11092  genpnnp  11093  genpnmax  11095  addclprlem1  11104  addclprlem2  11105  mulclprlem  11107  distrlem4pr  11114  1idpr  11117  psslinpr  11119  prlem934  11121  ltaddpr  11122  ltexprlem2  11125  ltexprlem3  11126  ltexprlem6  11129  ltexprlem7  11130  prlem936  11135  reclem2pr  11136  reclem3pr  11137  reclem4pr  11138