Syntax Definition wsb 1750

Description: Extend wff definition to include proper substitution (read "the wff that results when 𝑦 is properly substituted for 𝑥 in wff 𝜑"). (Contributed by NM, 24-Jan-2006.)

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	setvar 𝑥
vy	setvar 𝑦

Assertion

Ref	Expression
wsb	wff [𝑦 / 𝑥]𝜑

See definition df-sb 1751 for more information.