Syntax definition wsbc

Description: Extend wff notation to include the proper substitution of a class for a set. Read this notation as "the proper substitution of class A for setvar variable x in wff ph ".

	Ref	Expression
Assertion	wsbc	$$wff\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$