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 φ").

Hypotheses

Ref	Expression
wph	wff φ
vx	set x
vy	set y

Assertion

Ref	Expression
wsb	wff [y / x]φ

See definition df-sb 853 for more information.

metamath.org