Description: Existential quantification over a given variable is idempotent. Weak version of bj-exexbiex , requiring fewer axioms. (Contributed by GG, 4-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | exexw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| Assertion | exexw | |- ( E. x ph <-> E. x E. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exexw.1 | |- ( x = y -> ( ph <-> ps ) ) |
|
| 2 | 1 | notbid | |- ( x = y -> ( -. ph <-> -. ps ) ) |
| 3 | 2 | hba1w | |- ( A. x -. ph -> A. x A. x -. ph ) |
| 4 | 2 | spw | |- ( A. x -. ph -> -. ph ) |
| 5 | 4 | alimi | |- ( A. x A. x -. ph -> A. x -. ph ) |
| 6 | 3 5 | impbii | |- ( A. x -. ph <-> A. x A. x -. ph ) |
| 7 | 6 | notbii | |- ( -. A. x -. ph <-> -. A. x A. x -. ph ) |
| 8 | df-ex | |- ( E. x ph <-> -. A. x -. ph ) |
|
| 9 | 2exnaln | |- ( E. x E. x ph <-> -. A. x A. x -. ph ) |
|
| 10 | 7 8 9 | 3bitr4i | |- ( E. x ph <-> E. x E. x ph ) |