Definition df-csb

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)

	Ref	Expression
Assertion	df-csb	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		vx	|- x
2		cB	|- B
3	1 0 2	csb	|- [_ A / x ]_ B
4		vy	|- y
5	4	cv	|- y
6	5 2	wcel	|- y e. B
7	6 1 0	wsbc	|- [. A / x ]. y e. B
8	7 4	cab	|- { y | [. A / x ]. y e. B }
9	3 8	wceq	|- [_ A / x ]_ B = { y | [. A / x ]. y e. B }