Definition df-csb 3893

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 3776, to prevent ambiguity. Theorem sbcel1g 4412 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 4405). Theorem sbccsb 4432 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 3892	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2107	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3776	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2710	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3894  csbeq1  3895  csbeq2  3897  csbeq2d  3898  cbvcsbw  3902  cbvcsb  3903  csbid  3905  csbcow  3907  csbco  3908  csbtt  3909  csbconstg  3911  csbgfi  3913  nfcsb1d  3915  nfcsbd  3918  nfcsbw  3919  csbie  3928  csbied  3930  csbie2g  3935  cbvralcsf  3937  cbvreucsf  3939  cbvrabcsf  3940  csbprc  4405  sbcel12  4407  sbceqg  4408  csbnestgfw  4418  csbnestgf  4423  csbvarg  4430  csbexg  5309  bj-csbsnlem  35721  bj-csbprc  35728  csbcom2fi  36934