![]() |
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 10933 | . . 3 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q) | |
2 | 1 | pssssd 4062 | . 2 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q) |
3 | 2 | sselda 3949 | 1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ Q) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 Qcnq 10795 Pcnp 10802 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-3an 1090 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-ne 2945 df-ral 3066 df-rex 3075 df-v 3450 df-in 3922 df-ss 3932 df-pss 3934 df-np 10924 |
This theorem is referenced by: prub 10937 genpv 10942 genpdm 10945 genpss 10947 genpnnp 10948 genpnmax 10950 addclprlem1 10959 addclprlem2 10960 mulclprlem 10962 distrlem4pr 10969 1idpr 10972 psslinpr 10974 prlem934 10976 ltaddpr 10977 ltexprlem2 10980 ltexprlem3 10981 ltexprlem6 10984 ltexprlem7 10985 prlem936 10990 reclem2pr 10991 reclem3pr 10992 reclem4pr 10993 |
Copyright terms: Public domain | W3C validator |