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 3771, to prevent ambiguity. Theorem sbcel1g 4364 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 4357). Theorem sbccsb 4384 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 3882 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1527 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2105 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3771 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2799 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1528 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3884 csbeq1 3885 csbeq2 3887 csbeq2d 3888 cbvcsbw 3892 cbvcsb 3893 csbid 3895 csbcow 3897 csbco 3898 csbtt 3899 csbgfi 3902 nfcsb1d 3904 nfcsbd 3907 nfcsbw 3908 csbie2g 3922 cbvralcsf 3924 cbvreucsf 3926 cbvrabcsf 3927 csbprc 4357 sbcel12 4359 sbceqg 4360 csbnestgfw 4370 csbnestgf 4375 csbvarg 4382 csbexg 5206 bj-csbsnlem 34118 bj-csbprc 34124 csbcom2fi 35289 |
Copyright terms: Public domain | W3C validator |