Definition df-csb 3891

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 3775, to prevent ambiguity. Theorem sbcel1g 4409 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 4402). Theorem sbccsb 4429 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 3890	. 2 class ⦋𝐴 / 𝑥⦌𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1533	. . . . 5 class 𝑦
7	6, 3	wcel 2099	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wsbc 3775	. . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵
9	8, 5	cab 2705	. 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
10	4, 9	wceq 1534	1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}

This definition is referenced by:  csb2  3892  csbeq1  3893  csbeq2  3895  csbeq2d  3896  cbvcsbw  3900  cbvcsb  3901  csbid  3903  csbcow  3905  csbco  3906  csbtt  3907  csbconstg  3909  csbgfi  3911  nfcsb1d  3913  nfcsbd  3916  nfcsbw  3917  csbie  3926  csbied  3928  csbie2g  3933  cbvralcsf  3935  cbvreucsf  3937  cbvrabcsf  3938  csbprc  4402  sbcel12  4404  sbceqg  4405  csbnestgfw  4415  csbnestgf  4420  csbvarg  4427  csbexg  5304  bj-csbsnlem  36375  bj-csbprc  36382  csbcom2fi  37595