Definition df-csb 3895

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

This definition is referenced by:  csb2  3896  csbeq1  3897  csbeq2  3899  csbeq2d  3900  cbvcsbw  3904  cbvcsb  3905  csbid  3907  csbcow  3909  csbco  3910  csbtt  3911  csbconstg  3913  csbgfi  3915  nfcsb1d  3917  nfcsbd  3920  nfcsbw  3921  csbie  3930  csbied  3932  csbie2g  3937  cbvralcsf  3939  cbvreucsf  3941  cbvrabcsf  3942  csbprc  4407  sbcel12  4409  sbceqg  4410  csbnestgfw  4420  csbnestgf  4425  csbvarg  4432  csbexg  5311  bj-csbsnlem  35831  bj-csbprc  35838  csbcom2fi  37044