Theorem elprnq 10964

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145  Qcnq 10825  Pcnp 10832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-v 3459  df-ss 3924  df-pss 3927  df-np 10954

This theorem is referenced by:  prub  10967  genpv  10972  genpdm  10975  genpss  10977  genpnnp  10978  genpnmax  10980  addclprlem1  10989  addclprlem2  10990  mulclprlem  10992  distrlem4pr  10999  1idpr  11002  psslinpr  11004  prlem934  11006  ltaddpr  11007  ltexprlem2  11010  ltexprlem3  11011  ltexprlem6  11014  ltexprlem7  11015  prlem936  11020  reclem2pr  11021  reclem3pr  11022  reclem4pr  11023