Definition df-csb 3829

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 3720, to prevent ambiguity. Theorem sbcel1g 4321 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 4313). Theorem sbccsb 4341 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 3828	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1537	. . . . 5 class 𝑦
7	6, 3	wcel 2111	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3720	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2776	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1538	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3830  csbeq1  3831  csbeq2  3833  csbeq2d  3834  cbvcsbw  3838  cbvcsb  3839  csbid  3841  csbcow  3843  csbco  3844  csbtt  3845  csbgfi  3848  nfcsb1d  3850  nfcsbd  3853  nfcsbw  3854  csbie2g  3868  cbvralcsf  3870  cbvreucsf  3872  cbvrabcsf  3873  csbprc  4313  csb0  4314  sbcel12  4316  sbceqg  4317  csbnestgfw  4327  csbnestgf  4332  csbvarg  4339  csbexg  5178  bj-csbsnlem  34344  bj-csbprc  34350  csbcom2fi  35566