# Metamath Proof Explorer

## Theorem sbn

Description: Negation inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993) (Proof shortened by Wolf Lammen, 30-Apr-2018) Revise df-sb . (Revised by BJ, 25-Dec-2020)

Ref Expression
Assertion sbn ${⊢}\left[{t}/{x}\right]¬{\phi }↔¬\left[{t}/{x}\right]{\phi }$

### Proof

Step Hyp Ref Expression
1 df-sb ${⊢}\left[{t}/{x}\right]¬{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)$
2 alinexa ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)$
3 2 imbi2i ${⊢}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)↔\left({y}={t}\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)$
4 3 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to ¬{\phi }\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)$
5 alinexa ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)↔¬\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)$
6 dfsb7 ${⊢}\left[{t}/{x}\right]{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\wedge \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)$
7 5 6 xchbinxr ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={t}\to ¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\wedge {\phi }\right)\right)↔¬\left[{t}/{x}\right]{\phi }$
8 1 4 7 3bitri ${⊢}\left[{t}/{x}\right]¬{\phi }↔¬\left[{t}/{x}\right]{\phi }$