![]() |
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 3674, to prevent ambiguity. Theorem sbcel1g 4245 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 4238). Theorem sbccsb 4263 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 3779 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1507 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2051 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3674 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2751 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1508 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3781 csbeq1 3782 csbeq2 3783 cbvcsb 3784 csbid 3787 csbco 3789 csbtt 3790 csbgfi 3793 nfcsb1d 3795 nfcsbd 3798 csbie2g 3812 cbvralcsf 3813 cbvreucsf 3815 cbvrabcsf 3816 csbprc 4238 sbcel12 4240 sbceqg 4241 csbeq2d 4249 csbnestgf 4254 csbvarg 4261 csbexg 5067 bj-csbsnlem 33749 bj-csbprc 33755 csbcom2fi 34887 |
Copyright terms: Public domain | W3C validator |