Theorem elprnq 10994

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  Qcnq 10855  Pcnp 10862

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-v 3460  df-ss 3925  df-pss 3928  df-np 10984

This theorem is used by:  prub  10997  genpv  11002  genpdm  11005  genpss  11007  genpnnp  11008  genpnmax  11010  addclprlem1  11019  addclprlem2  11020  mulclprlem  11022  distrlem4pr  11029  1idpr  11032  psslinpr  11034  prlem934  11036  ltaddpr  11037  ltexprlem2  11040  ltexprlem3  11041  ltexprlem6  11044  ltexprlem7  11045  prlem936  11050  reclem2pr  11051  reclem3pr  11052  reclem4pr  11053