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

Proof

Step Hyp Ref Expression
1 dfsb 
 |-  ( [ 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 )