wsb - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > wsb		Structured version Visualization version GIF version

Syntax Definition wsb 2063

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 2064 for more information.

Colors of variables: wff setvar class

W3C validator