![]() |
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 2758, to prevent ambiguity. Theorem sbcel1g 2863 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2872 recreates substitution into a wff from this definition. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
df-csb | ⊢ ⦋A / x⦌B = {y ∣ [A / x]y ∈ B} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar x | |
2 | cA | . . 3 class A | |
3 | cB | . . 3 class B | |
4 | 1, 2, 3 | csb 2846 | . 2 class ⦋A / x⦌B |
5 | vy | . . . . . 6 setvar y | |
6 | 5 | cv 1241 | . . . . 5 class y |
7 | 6, 3 | wcel 1390 | . . . 4 wff y ∈ B |
8 | 7, 1, 2 | wsbc 2758 | . . 3 wff [A / x]y ∈ B |
9 | 8, 5 | cab 2023 | . 2 class {y ∣ [A / x]y ∈ B} |
10 | 4, 9 | wceq 1242 | 1 wff ⦋A / x⦌B = {y ∣ [A / x]y ∈ B} |
Colors of variables: wff set class |
This definition is referenced by: csb2 2848 csbeq1 2849 cbvcsb 2850 csbid 2853 csbco 2855 csbtt 2856 sbcel12g 2859 sbceqg 2860 csbeq2d 2868 csbvarg 2871 nfcsb1d 2874 nfcsbd 2877 csbie2g 2890 csbnestgf 2892 cbvralcsf 2902 cbvrexcsf 2903 cbvreucsf 2904 cbvrabcsf 2905 csbprc 3256 csbexga 3876 bdccsb 9315 |
Copyright terms: Public domain | W3C validator |