Description: Change bound variable. Uses only Tarski's FOL axiom schemes. Part of Lemma 7 of KalishMontague p. 86. (Contributed by Wolf Lammen, 5-Mar-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | wl-moteq | |- ( E* x T. -> y = z ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-mo | |- ( E* x T. <-> E. w A. x ( T. -> x = w ) ) |
|
| 2 | stdpc5v | |- ( A. x ( T. -> x = w ) -> ( T. -> A. x x = w ) ) |
|
| 3 | tru | |- T. |
|
| 4 | 3 | pm2.24i | |- ( -. T. -> y = z ) |
| 5 | aeveq | |- ( A. x x = w -> y = z ) |
|
| 6 | 4 5 | ja | |- ( ( T. -> A. x x = w ) -> y = z ) |
| 7 | 2 6 | syl | |- ( A. x ( T. -> x = w ) -> y = z ) |
| 8 | 7 | exlimiv | |- ( E. w A. x ( T. -> x = w ) -> y = z ) |
| 9 | 1 8 | sylbi | |- ( E* x T. -> y = z ) |