Metamath Proof Explorer

Syntax definition wrnf

Description: Syntax for restricted nonfreeness.

Ref Expression
Assertion wrnf 
wff F/ x e. A ph