Definition df-csb 3833

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 3724, to prevent ambiguity. Theorem sbcel1g 4346 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 4339). Theorem sbccsb 4366 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 3832	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1547	. . . . 5 class 𝑦
7	6, 3	wcel 2121	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3724	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2719	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1548	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3834  csbeq1  3835  csbeq2  3837  csbeq2d  3838  csbeq2dv  3839  cbvcsbw  3842  cbvcsb  3843  cbvcsbv  3844  csbid  3845  csbcow  3847  csbco  3848  csbtt  3849  csbconstg  3851  csbgfi  3852  nfcsb1d  3854  nfcsbd  3857  nfcsbw  3858  csbie  3867  csbied  3868  csbie2g  3872  cbvralcsf  3874  cbvreucsf  3876  cbvrabcsf  3877  csbprc  4339  sbcel12  4341  sbceqg  4342  csbnestgfw  4352  csbnestgf  4357  csbvarg  4364  csbexg  5234  cbvcsbvw2  36472  cbvcsbdavw  36500  cbvcsbdavw2  36501  bj-csbsnlem  37269  bj-csbprc  37276  csbcom2fi  38508