Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elprnq | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
elprnq | ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ Q) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prpssnq 10604 | . . 3 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q) | |
2 | 1 | pssssd 4012 | . 2 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q) |
3 | 2 | sselda 3901 | 1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ Q) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∈ wcel 2110 Qcnq 10466 Pcnp 10473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-3an 1091 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3066 df-rex 3067 df-v 3410 df-in 3873 df-ss 3883 df-pss 3885 df-np 10595 |
This theorem is referenced by: prub 10608 genpv 10613 genpdm 10616 genpss 10618 genpnnp 10619 genpnmax 10621 addclprlem1 10630 addclprlem2 10631 mulclprlem 10633 distrlem4pr 10640 1idpr 10643 psslinpr 10645 prlem934 10647 ltaddpr 10648 ltexprlem2 10651 ltexprlem3 10652 ltexprlem6 10655 ltexprlem7 10656 prlem936 10661 reclem2pr 10662 reclem3pr 10663 reclem4pr 10664 |
Copyright terms: Public domain | W3C validator |