Definition df-csb 3834

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 3725, 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 3833	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3725	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2713	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3835  csbeq1  3836  csbeq2  3838  csbeq2d  3839  csbeq2dv  3840  cbvcsbw  3843  cbvcsb  3844  cbvcsbv  3845  csbid  3846  csbcow  3848  csbco  3849  csbtt  3850  csbconstg  3852  csbgfi  3853  nfcsb1d  3855  nfcsbd  3858  nfcsbw  3859  csbie  3868  csbied  3869  csbie2g  3873  cbvralcsf  3875  cbvreucsf  3877  cbvrabcsf  3878  csbprc  4339  sbcel12  4341  sbceqg  4342  csbnestgfw  4352  csbnestgf  4357  csbvarg  4364  csbexg  5234  cbvcsbvw2  36401  cbvcsbdavw  36429  cbvcsbdavw2  36430  bj-csbsnlem  37198  bj-csbprc  37205  csbcom2fi  38437