Metamath Proof Explorer


Syntax definition wnf

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

Ref Expression
Assertion wnf
wff F/ x ph