Metamath Proof Explorer


Syntax definition wsb

Description: Extend wff definition to include proper substitution. Read: "the wff that results when y is properly substituted for x in wff ph ". (Contributed by NM, 24-Jan-2006)

Ref Expression
Assertion wsb
wff [ y / x ] ph