This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ [t/ x] \neg φ \leftrightarrow \neg [t/ x] φ$

Proof

Step	Hyp	Ref	Expression
1		dfsb	$⊢ [t/ x] \neg φ \leftrightarrow \forall y (y = t \to \forall x (x = y \to \neg φ))$
2		alinexa	$⊢ \forall x (x = y \to \neg φ) \leftrightarrow \neg \exists x (x = y \land φ)$
3	2	imbi2i	$⊢ (y = t \to \forall x (x = y \to \neg φ)) \leftrightarrow (y = t \to \neg \exists x (x = y \land φ))$
4	3	albii	$⊢ \forall y (y = t \to \forall x (x = y \to \neg φ)) \leftrightarrow \forall y (y = t \to \neg \exists x (x = y \land φ))$
5		alinexa	$⊢ \forall y (y = t \to \neg \exists x (x = y \land φ)) \leftrightarrow \neg \exists y (y = t \land \exists x (x = y \land φ))$
6		dfsb7	$⊢ [t/ x] φ \leftrightarrow \exists y (y = t \land \exists x (x = y \land φ))$
7	5 6	xchbinxr	$⊢ \forall y (y = t \to \neg \exists x (x = y \land φ)) \leftrightarrow \neg [t/ x] φ$
8	1 4 7	3bitri	$⊢ [t/ x] \neg φ \leftrightarrow \neg [t/ x] φ$