Description: Equality theorem for restricted unique existential quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 5-Apr-2004) (Revised by Andrew Salmon, 11-Jul-2011)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | rmoeq1f.1 | |- F/_ x A |
|
| rmoeq1f.2 | |- F/_ x B |
||
| Assertion | reueq1f | |- ( A = B -> ( E! x e. A ph <-> E! x e. B ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rmoeq1f.1 | |- F/_ x A |
|
| 2 | rmoeq1f.2 | |- F/_ x B |
|
| 3 | 1 2 | rexeqf | |- ( A = B -> ( E. x e. A ph <-> E. x e. B ph ) ) |
| 4 | 1 2 | rmoeq1f | |- ( A = B -> ( E* x e. A ph <-> E* x e. B ph ) ) |
| 5 | 3 4 | anbi12d | |- ( A = B -> ( ( E. x e. A ph /\ E* x e. A ph ) <-> ( E. x e. B ph /\ E* x e. B ph ) ) ) |
| 6 | reu5 | |- ( E! x e. A ph <-> ( E. x e. A ph /\ E* x e. A ph ) ) |
|
| 7 | reu5 | |- ( E! x e. B ph <-> ( E. x e. B ph /\ E* x e. B ph ) ) |
|
| 8 | 5 6 7 | 3bitr4g | |- ( A = B -> ( E! x e. A ph <-> E! x e. B ph ) ) |