Metamath Proof Explorer

Syntax definition wrnf

Description: Syntax for restricted nonfreeness.

Ref Expression
Assertion wrnf wff Ⅎ x ∈ A φ