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 ] -. ph <-> -. [ t / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		df-sb	|- ( [ t / x ] -. ph <-> A. y ( y = t -> A. x ( x = y -> -. ph ) ) )
2		alinexa	|- ( A. x ( x = y -> -. ph ) <-> -. E. x ( x = y /\ ph ) )
3	2	imbi2i	|- ( ( y = t -> A. x ( x = y -> -. ph ) ) <-> ( y = t -> -. E. x ( x = y /\ ph ) ) )
4	3	albii	|- ( A. y ( y = t -> A. x ( x = y -> -. ph ) ) <-> A. y ( y = t -> -. E. x ( x = y /\ ph ) ) )
5		alinexa	|- ( A. y ( y = t -> -. E. x ( x = y /\ ph ) ) <-> -. E. y ( y = t /\ E. x ( x = y /\ ph ) ) )
6		dfsb7	|- ( [ t / x ] ph <-> E. y ( y = t /\ E. x ( x = y /\ ph ) ) )
7	5 6	xchbinxr	|- ( A. y ( y = t -> -. E. x ( x = y /\ ph ) ) <-> -. [ t / x ] ph )
8	1 4 7	3bitri	|- ( [ t / x ] -. ph <-> -. [ t / x ] ph )