Definition df-csb 3830

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 3712, to prevent ambiguity. Theorem sbcel1g 4345 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 4338). Theorem sbccsb 4365 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 3829	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1542	. . . . 5 class 𝑦
7	6, 3	wcel 2112	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3712	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2716	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1543	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3831  csbeq1  3832  csbeq2  3834  csbeq2d  3835  cbvcsbw  3839  cbvcsb  3840  csbid  3842  csbcow  3844  csbco  3845  csbtt  3846  csbconstg  3848  csbgfi  3850  nfcsb1d  3852  nfcsbd  3855  nfcsbw  3856  csbie  3865  csbied  3867  csbie2g  3872  cbvralcsf  3874  cbvreucsf  3876  cbvrabcsf  3877  csbprc  4338  sbcel12  4340  sbceqg  4341  csbnestgfw  4351  csbnestgf  4356  csbvarg  4363  csbexg  5227  bj-csbsnlem  34990  bj-csbprc  34997  csbcom2fi  36192