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 10412 | . . 3 ⊢ (𝐴 ∈ P → 𝐴 ⊊ Q) | |
2 | 1 | pssssd 4074 | . 2 ⊢ (𝐴 ∈ P → 𝐴 ⊆ Q) |
3 | 2 | sselda 3967 | 1 ⊢ ((𝐴 ∈ P ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ Q) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∈ wcel 2114 Qcnq 10274 Pcnp 10281 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-v 3496 df-in 3943 df-ss 3952 df-pss 3954 df-np 10403 |
This theorem is referenced by: prub 10416 genpv 10421 genpdm 10424 genpss 10426 genpnnp 10427 genpnmax 10429 addclprlem1 10438 addclprlem2 10439 mulclprlem 10441 distrlem4pr 10448 1idpr 10451 psslinpr 10453 prlem934 10455 ltaddpr 10456 ltexprlem2 10459 ltexprlem3 10460 ltexprlem6 10463 ltexprlem7 10464 prlem936 10469 reclem2pr 10470 reclem3pr 10471 reclem4pr 10472 |
Copyright terms: Public domain | W3C validator |