Description: Equality theorem for restricted universal quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004) (Revised by Andrew Salmon, 11-Jul-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | raleq1f.1 | |- F/_ x A |
|
| raleq1f.2 | |- F/_ x B |
||
| Assertion | raleqf | |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | raleq1f.1 | |- F/_ x A |
|
| 2 | raleq1f.2 | |- F/_ x B |
|
| 3 | 1 2 | nfeq | |- F/ x A = B |
| 4 | eleq2 | |- ( A = B -> ( x e. A <-> x e. B ) ) |
|
| 5 | 4 | imbi1d | |- ( A = B -> ( ( x e. A -> ph ) <-> ( x e. B -> ph ) ) ) |
| 6 | 3 5 | albid | |- ( A = B -> ( A. x ( x e. A -> ph ) <-> A. x ( x e. B -> ph ) ) ) |
| 7 | df-ral | |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) ) |
|
| 8 | df-ral | |- ( A. x e. B ph <-> A. x ( x e. B -> ph ) ) |
|
| 9 | 6 7 8 | 3bitr4g | |- ( A = B -> ( A. x e. A ph <-> A. x e. B ph ) ) |