Description: Specialization. Lemma 8 of KalishMontague p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017) (Proof shortened by Wolf Lammen, 7-Aug-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | spimw.1 | |- ( -. ps -> A. x -. ps ) |
|
| spimw.2 | |- ( x = y -> ( ph -> ps ) ) |
||
| Assertion | spimw | |- ( A. x ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | spimw.1 | |- ( -. ps -> A. x -. ps ) |
|
| 2 | spimw.2 | |- ( x = y -> ( ph -> ps ) ) |
|
| 3 | ax6v | |- -. A. x -. x = y |
|
| 4 | 1 2 | spimfw | |- ( -. A. x -. x = y -> ( A. x ph -> ps ) ) |
| 5 | 3 4 | ax-mp | |- ( A. x ph -> ps ) |