Metamath Proof Explorer


Syntax definition wnfc

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

Ref Expression
Assertion wnfc
wff F/_ x A