# Metamath Proof Explorer

## Theorem wl-equsb4

Description: Substitution applied to an atomic wff. The distinctor antecedent is more general than a distinct variable constraint. (Contributed by Wolf Lammen, 26-Jun-2019)

Ref Expression
Assertion wl-equsb4 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(\left[{y}/{x}\right]{y}={z}↔{y}={z}\right)$

### Proof

Step Hyp Ref Expression
1 nfeqf ${⊢}\left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={z}$
2 1 ex ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={z}\right)$
3 sbft ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={z}\to \left(\left[{y}/{x}\right]{y}={z}↔{y}={z}\right)$
4 2 3 syl6com ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left[{y}/{x}\right]{y}={z}↔{y}={z}\right)\right)$
5 sbequ12r ${⊢}{y}={x}\to \left(\left[{y}/{x}\right]{y}={z}↔{y}={z}\right)$
6 5 equcoms ${⊢}{x}={y}\to \left(\left[{y}/{x}\right]{y}={z}↔{y}={z}\right)$
7 6 sps ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \left(\left[{y}/{x}\right]{y}={z}↔{y}={z}\right)$
8 4 7 pm2.61d2 ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={z}\to \left(\left[{y}/{x}\right]{y}={z}↔{y}={z}\right)$