![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-csb | Unicode 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 2826, to prevent ambiguity. Theorem sbcel1g 2936 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2945 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
![]() ![]() | |
2 | cA |
. . 3
![]() ![]() | |
3 | cB |
. . 3
![]() ![]() | |
4 | 1, 2, 3 | csb 2919 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vy |
. . . . . 6
![]() ![]() | |
6 | 5 | cv 1284 |
. . . . 5
![]() ![]() |
7 | 6, 3 | wcel 1434 |
. . . 4
![]() ![]() ![]() ![]() |
8 | 7, 1, 2 | wsbc 2826 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8, 5 | cab 2069 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 4, 9 | wceq 1285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: csb2 2921 csbeq1 2922 cbvcsb 2923 csbid 2926 csbco 2928 csbtt 2929 sbcel12g 2932 sbceqg 2933 csbeq2d 2941 csbvarg 2944 nfcsb1d 2947 nfcsbd 2950 csbie2g 2963 csbnestgf 2965 cbvralcsf 2975 cbvrexcsf 2976 cbvreucsf 2977 cbvrabcsf 2978 csbprc 3310 csbexga 3932 bdccsb 11094 |
Copyright terms: Public domain | W3C validator |