# Metamath Proof Explorer

## Theorem speimfw

Description: Specialization, with additional weakening (compared to 19.2 ) to allow bundling of x and y . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017) (Proof shortened by Wolf Lammen, 5-Dec-2017)

Ref Expression
Hypothesis speimfw.2 ${⊢}{x}={y}\to \left({\phi }\to {\psi }\right)$
Assertion speimfw ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 speimfw.2 ${⊢}{x}={y}\to \left({\phi }\to {\psi }\right)$
2 df-ex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}$
3 2 biimpri ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}$
4 1 com12 ${⊢}{\phi }\to \left({x}={y}\to {\psi }\right)$
5 4 aleximi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
6 3 5 syl5com ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{x}={y}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\psi }\right)$