Description: Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rexrp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elrp | |
|
2 | 1 | anbi1i | |
3 | anass | |
|
4 | 2 3 | bitri | |
5 | 4 | rexbii2 | |