Syntax Definition wsb 852

Description: Extend wff definition to include proper substitution (read "the wff that results when y is properly substituted for x in wff ph").

Hypotheses

Ref	Expression
wph	wff ph
vx	set x
vy	set y

Assertion

Ref	Expression
wsb	wff [y / x]ph

See definition df-sb 853 for more information.

metamath.org