Metamath Proof Explorer


Theorem nf2

Description: Alternate definition of nonfreeness. (Contributed by BJ, 16-Sep-2021)

Ref Expression
Assertion nf2 x φ x φ ¬ x φ

Proof

Step Hyp Ref Expression
1 df-nf x φ x φ x φ
2 imor x φ x φ ¬ x φ x φ
3 orcom ¬ x φ x φ x φ ¬ x φ
4 1 2 3 3bitri x φ x φ ¬ x φ