Description: Define the proper substitution of a class for a set into another class.
The underlined brackets distinguish it from the substitution into a wff,
wsbc , to prevent ambiguity. Theorem sbcel1g shows an example of
how ambiguity could arise if we did not use distinguished brackets.
When A is a proper class, this evaluates to the empty set (see
csbprc ). Theorem sbccsb recovers substitution into a wff from this
definition. (Contributed by NM, 10-Nov-2005)