df-sb

Definition. Proper Substitution.

Description:

This definition (sb7 in set.mm) is adopted instead of Metamath's because it works for any set term y.

Arguments:

(st), (sv), (pr), (sv),

Distinct variable conditions:

(, ), (, ), (, ),

Assertions:

([/](()(())))