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=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		vx	$$setvarx$$
2		cB	$$classB$$
3	1 0 2	csb	$$class⦋A/x⦌B$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	5 2	wcel	$$wffy\in B$$
7	6 1 0	wsbc	$$wff\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B$$
8	7 4	cab	$$class\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$
9	3 8	wceq	$$wff⦋A/x⦌B=\left\{y|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}y\in B\right\}$$