Definition df-csb 3884

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 3772, to prevent ambiguity. Theorem sbcel1g 4365 shows an example of how ambiguity could arise if we did not use distinguished brackets. When 𝐴 is a proper class, this evaluates to the empty set (see csbprc 4358). Theorem sbccsb 4385 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
df-csb	⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

Distinct variable groups:   𝑦,𝐴   𝑦,𝐵   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-csb

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	csb 3883	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1536	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3772	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2799	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1537	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3885  csbeq1  3886  csbeq2  3888  csbeq2d  3889  cbvcsbw  3893  cbvcsb  3894  csbid  3896  csbcow  3898  csbco  3899  csbtt  3900  csbgfi  3903  nfcsb1d  3905  nfcsbd  3908  nfcsbw  3909  csbie2g  3923  cbvralcsf  3925  cbvreucsf  3927  cbvrabcsf  3928  csbprc  4358  sbcel12  4360  sbceqg  4361  csbnestgfw  4371  csbnestgf  4376  csbvarg  4383  csbexg  5214  bj-csbsnlem  34223  bj-csbprc  34229  csbcom2fi  35421