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 2909, to prevent ambiguity. Theorem sbcel1g 3021 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsbg 3031 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 3003 | . 2 |
5 | vy | . . . . . 6 | |
6 | 5 | cv 1330 | . . . . 5 |
7 | 6, 3 | wcel 1480 | . . . 4 |
8 | 7, 1, 2 | wsbc 2909 | . . 3 |
9 | 8, 5 | cab 2125 | . 2 |
10 | 4, 9 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: csb2 3005 csbeq1 3006 cbvcsbw 3007 cbvcsb 3008 csbid 3011 csbco 3013 csbtt 3014 sbcel12g 3017 sbceqg 3018 csbeq2 3026 csbeq2d 3027 csbvarg 3030 nfcsb1d 3033 nfcsbd 3036 csbie2g 3050 csbnestgf 3052 cbvralcsf 3062 cbvrexcsf 3063 cbvreucsf 3064 cbvrabcsf 3065 csbprc 3408 csbexga 4056 bdccsb 13058 |
Copyright terms: Public domain | W3C validator |