Description: A version of rzal using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 20-Apr-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | rzalf.1 | |- F/ x A = (/) |
|
| Assertion | rzalf | |- ( A = (/) -> A. x e. A ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rzalf.1 | |- F/ x A = (/) |
|
| 2 | ne0i | |- ( x e. A -> A =/= (/) ) |
|
| 3 | 2 | necon2bi | |- ( A = (/) -> -. x e. A ) |
| 4 | 3 | pm2.21d | |- ( A = (/) -> ( x e. A -> ph ) ) |
| 5 | 1 4 | ralrimi | |- ( A = (/) -> A. x e. A ph ) |