This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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