Metamath Proof Explorer


Syntax definition wnf

Description: Extend wff definition to include the not-free predicate.

Ref Expression
Assertion wnf wff 𝑥 𝜑