Definition df-csb 3839

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 3729, to prevent ambiguity. Theorem sbcel1g 4357 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 4350). Theorem sbccsb 4377 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 3838	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3729	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2715	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3840  csbeq1  3841  csbeq2  3843  csbeq2d  3844  csbeq2dv  3845  cbvcsbw  3848  cbvcsb  3849  cbvcsbv  3850  csbid  3851  csbcow  3853  csbco  3854  csbtt  3855  csbconstg  3857  csbgfi  3858  nfcsb1d  3860  nfcsbd  3863  nfcsbw  3864  csbie  3873  csbied  3874  csbie2g  3878  cbvralcsf  3880  cbvreucsf  3882  cbvrabcsf  3883  csbprc  4350  sbcel12  4352  sbceqg  4353  csbnestgfw  4363  csbnestgf  4368  csbvarg  4375  csbexg  5246  cbvcsbvw2  36410  cbvcsbdavw  36438  cbvcsbdavw2  36439  bj-csbsnlem  37207  bj-csbprc  37214  csbcom2fi  38446