Metamath Proof Explorer

Theorem nfnbi

Description: A variable is non-free in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019)

Ref Expression
Assertion nfnbi 
|- ( F/ x ph <-> F/ x -. ph )

Proof

Step Hyp Ref Expression
1 orcom 
 |-  ( ( A. x ph \/ A. x -. ph ) <-> ( A. x -. ph \/ A. x ph ) )
2 nf3 
 |-  ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )
3 nf3 
 |-  ( F/ x -. ph <-> ( A. x -. ph \/ A. x -. -. ph ) )
4 notnotb 
 |-  ( ph <-> -. -. ph )
5 4 albii 
 |-  ( A. x ph <-> A. x -. -. ph )
6 5 orbi2i 
 |-  ( ( A. x -. ph \/ A. x ph ) <-> ( A. x -. ph \/ A. x -. -. ph ) )
7 3 6 bitr4i 
 |-  ( F/ x -. ph <-> ( A. x -. ph \/ A. x ph ) )
8 1 2 7 3bitr4i 
 |-  ( F/ x ph <-> F/ x -. ph )