Metamath Proof Explorer


Theorem nf3

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

Ref Expression
Assertion nf3 x φ x φ x ¬ φ

Proof

Step Hyp Ref Expression
1 nf2 x φ x φ ¬ x φ
2 alnex x ¬ φ ¬ x φ
3 2 orbi2i x φ x ¬ φ x φ ¬ x φ
4 1 3 bitr4i x φ x φ x ¬ φ