Definition df-csb 3922

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 3804, to prevent ambiguity. Theorem sbcel1g 4439 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 4432). Theorem sbccsb 4459 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 3921	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1536	. . . . 5 class 𝑦
7	6, 3	wcel 2108	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3804	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2717	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1537	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3923  csbeq1  3924  csbeq2  3926  csbeq2d  3927  csbeq2dv  3928  cbvcsbw  3931  cbvcsb  3932  cbvcsbv  3933  csbid  3934  csbcow  3936  csbco  3937  csbtt  3938  csbconstg  3940  csbgfi  3942  nfcsb1d  3944  nfcsbd  3947  nfcsbw  3948  csbie  3957  csbied  3959  csbie2g  3964  cbvralcsf  3966  cbvreucsf  3968  cbvrabcsf  3969  csbprc  4432  sbcel12  4434  sbceqg  4435  csbnestgfw  4445  csbnestgf  4450  csbvarg  4457  csbexg  5328  cbvcsbvw2  36197  cbvcsbdavw  36225  cbvcsbdavw2  36226  bj-csbsnlem  36869  bj-csbprc  36876  csbcom2fi  38088