Syntax Definition wsub 207

Description: Proper substitution of x with Y. Although used as a primitive token in the axioms, it can actually be treated as a defined symbol; see dfsub 233. See nsub 277 for proper substitution in nilads.

Hypotheses

Ref	Expression
wph	wff 𝜑
vx	var x
ny	nilad Y

Assertion

Ref	Expression
wsub	wff [x ≔ Y] 𝜑

This syntax is primitive. The first axiom using it is ax-subse1 220.