Metamath Proof Explorer


Theorem nfnbi

Description: A variable is nonfree in a proposition if and only if it is so in its negation. (Contributed by BJ, 6-May-2019) (Proof shortened by Wolf Lammen, 6-Oct-2024)

Ref Expression
Assertion nfnbi xφx¬φ

Proof

Step Hyp Ref Expression
1 exnal x¬φ¬xφ
2 1 imbi1i x¬φx¬φ¬xφx¬φ
3 df-nf x¬φx¬φx¬φ
4 nf4 xφ¬xφx¬φ
5 2 3 4 3bitr4ri xφx¬φ