Description: Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rexrp | |- ( E. x e. RR+ ph <-> E. x e. RR ( 0 < x /\ ph ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp | |- ( x e. RR+ <-> ( x e. RR /\ 0 < x ) ) |
|
2 | 1 | anbi1i | |- ( ( x e. RR+ /\ ph ) <-> ( ( x e. RR /\ 0 < x ) /\ ph ) ) |
3 | anass | |- ( ( ( 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 | rexbii2 | |- ( E. x e. RR+ ph <-> E. x e. RR ( 0 < x /\ ph ) ) |