Theorem elprnq 11057

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  Qcnq 10918  Pcnp 10925

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-pss 3919  df-np 11047

This theorem is used by:  prub  11060  genpv  11065  genpdm  11068  genpss  11070  genpnnp  11071  genpnmax  11073  addclprlem1  11082  addclprlem2  11083  mulclprlem  11085  distrlem4pr  11092  1idpr  11095  psslinpr  11097  prlem934  11099  ltaddpr  11100  ltexprlem2  11103  ltexprlem3  11104  ltexprlem6  11107  ltexprlem7  11108  prlem936  11113  reclem2pr  11114  reclem3pr  11115  reclem4pr  11116