Description: Quantification over positive reals. (Contributed by NM, 12-Feb-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | ralrp | |- ( A. x e. RR+ ph <-> A. x e. RR ( 0 < x -> ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp | |- ( x e. RR+ <-> ( x e. RR /\ 0 < x ) ) |
|
2 | 1 | imbi1i | |- ( ( x e. RR+ -> ph ) <-> ( ( x e. RR /\ 0 < x ) -> ph ) ) |
3 | impexp | |- ( ( ( x e. RR /\ 0 < x ) -> ph ) <-> ( x e. RR -> ( 0 < x -> ph ) ) ) |
|
4 | 2 3 | bitri | |- ( ( x e. RR+ -> ph ) <-> ( x e. RR -> ( 0 < x -> ph ) ) ) |
5 | 4 | ralbii2 | |- ( A. x e. RR+ ph <-> A. x e. RR ( 0 < x -> ph ) ) |