| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-csb | Structured version Visualization version GIF version | ||
| 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 3788, to prevent ambiguity. Theorem sbcel1g 4416 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 4409). Theorem sbccsb 4436 recovers substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.) |
| Ref | Expression |
|---|---|
| df-csb | ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx | . . 3 setvar 𝑥 | |
| 2 | cA | . . 3 class 𝐴 | |
| 3 | cB | . . 3 class 𝐵 | |
| 4 | 1, 2, 3 | csb 3899 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
| 5 | vy | . . . . . 6 setvar 𝑦 | |
| 6 | 5 | cv 1539 | . . . . 5 class 𝑦 |
| 7 | 6, 3 | wcel 2108 | . . . 4 wff 𝑦 ∈ 𝐵 |
| 8 | 7, 1, 2 | wsbc 3788 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
| 9 | 8, 5 | cab 2714 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
| 10 | 4, 9 | wceq 1540 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
| Colors of variables: wff setvar class |
| This definition is referenced by: csb2 3901 csbeq1 3902 csbeq2 3904 csbeq2d 3905 csbeq2dv 3906 cbvcsbw 3909 cbvcsb 3910 cbvcsbv 3911 csbid 3912 csbcow 3914 csbco 3915 csbtt 3916 csbconstg 3918 csbgfi 3919 nfcsb1d 3921 nfcsbd 3924 nfcsbw 3925 csbie 3934 csbied 3935 csbie2g 3939 cbvralcsf 3941 cbvreucsf 3943 cbvrabcsf 3944 csbprc 4409 sbcel12 4411 sbceqg 4412 csbnestgfw 4422 csbnestgf 4427 csbvarg 4434 csbexg 5310 cbvcsbvw2 36232 cbvcsbdavw 36260 cbvcsbdavw2 36261 bj-csbsnlem 36904 bj-csbprc 36911 csbcom2fi 38135 |
| Copyright terms: Public domain | W3C validator |