Theorem elprnq 11004

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-v 3455  df-ss 3919  df-pss 3922  df-np 10994

This theorem is used by:  prub  11007  genpv  11012  genpdm  11015  genpss  11017  genpnnp  11018  genpnmax  11020  addclprlem1  11029  addclprlem2  11030  mulclprlem  11032  distrlem4pr  11039  1idpr  11042  psslinpr  11044  prlem934  11046  ltaddpr  11047  ltexprlem2  11050  ltexprlem3  11051  ltexprlem6  11054  ltexprlem7  11055  prlem936  11060  reclem2pr  11061  reclem3pr  11062  reclem4pr  11063