![]() |
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 2977, to prevent ambiguity. Theorem sbcel1g 3091 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3101 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 3072 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vy |
. . . . . 6
![]() ![]() | |
6 | 5 | cv 1363 |
. . . . 5
![]() ![]() |
7 | 6, 3 | wcel 2160 |
. . . 4
![]() ![]() ![]() ![]() |
8 | 7, 1, 2 | wsbc 2977 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8, 5 | cab 2175 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 4, 9 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: csb2 3074 csbeq1 3075 cbvcsbw 3076 cbvcsb 3077 csbid 3080 csbco 3082 csbcow 3083 csbtt 3084 sbcel12g 3087 sbceqg 3088 csbeq2 3096 csbeq2d 3097 csbvarg 3100 nfcsb1d 3103 nfcsbd 3107 nfcsbw 3108 csbie2g 3122 csbnestgf 3124 cbvralcsf 3134 cbvrexcsf 3135 cbvreucsf 3136 cbvrabcsf 3137 csbprc 3483 csbexga 4146 bdccsb 15049 |
Copyright terms: Public domain | W3C validator |