![]() |
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 2862, to prevent ambiguity. Theorem sbcel1g 2972 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 2981 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 2955 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vy |
. . . . . 6
![]() ![]() | |
6 | 5 | cv 1298 |
. . . . 5
![]() ![]() |
7 | 6, 3 | wcel 1448 |
. . . 4
![]() ![]() ![]() ![]() |
8 | 7, 1, 2 | wsbc 2862 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8, 5 | cab 2086 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 4, 9 | wceq 1299 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: csb2 2957 csbeq1 2958 cbvcsb 2959 csbid 2962 csbco 2964 csbtt 2965 sbcel12g 2968 sbceqg 2969 csbeq2d 2977 csbvarg 2980 nfcsb1d 2983 nfcsbd 2986 csbie2g 3000 csbnestgf 3002 cbvralcsf 3012 cbvrexcsf 3013 cbvreucsf 3014 cbvrabcsf 3015 csbprc 3355 csbexga 3996 bdccsb 12639 |
Copyright terms: Public domain | W3C validator |