Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-csb | 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 2882, to prevent ambiguity. Theorem sbcel1g 2992 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3001 recreates 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 2975 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1315 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 1465 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 2882 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2103 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1316 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff set class |
This definition is referenced by: csb2 2977 csbeq1 2978 cbvcsb 2979 csbid 2982 csbco 2984 csbtt 2985 sbcel12g 2988 sbceqg 2989 csbeq2d 2997 csbvarg 3000 nfcsb1d 3003 nfcsbd 3006 csbie2g 3020 csbnestgf 3022 cbvralcsf 3032 cbvrexcsf 3033 cbvreucsf 3034 cbvrabcsf 3035 csbprc 3378 csbexga 4026 bdccsb 12954 |
Copyright terms: Public domain | W3C validator |