Theorem elprnq 10977

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143  Qcnq 10838  Pcnp 10845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3923  df-pss 3926  df-np 10967

This theorem is referenced by:  prub  10980  genpv  10985  genpdm  10988  genpss  10990  genpnnp  10991  genpnmax  10993  addclprlem1  11002  addclprlem2  11003  mulclprlem  11005  distrlem4pr  11012  1idpr  11015  psslinpr  11017  prlem934  11019  ltaddpr  11020  ltexprlem2  11023  ltexprlem3  11024  ltexprlem6  11027  ltexprlem7  11028  prlem936  11033  reclem2pr  11034  reclem3pr  11035  reclem4pr  11036