![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-csb | Structured version Visualization version 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 3279, to prevent ambiguity. Theorem sbcel1g 3788 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3805 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 3375 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | vy |
. . . . . 6
![]() ![]() | |
6 | 5 | cv 1454 |
. . . . 5
![]() ![]() |
7 | 6, 3 | wcel 1898 |
. . . 4
![]() ![]() ![]() ![]() |
8 | 7, 1, 2 | wsbc 3279 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 8, 5 | cab 2448 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 4, 9 | wceq 1455 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3377 csbeq1 3378 csbeq2 3379 cbvcsb 3380 csbid 3383 csbco 3385 csbtt 3386 nfcsb1d 3389 nfcsbd 3392 csbie2g 3406 cbvralcsf 3407 cbvreucsf 3409 cbvrabcsf 3410 csbprc 3782 sbcel12 3784 sbceqg 3785 csbeq2d 3792 csbnestgf 3797 csbvarg 3804 csbexg 4551 bj-csbsnlem 31550 bj-csbprc 31556 csbcom2fi 32414 csbgfi 32415 sbcel12gOLD 36949 |
Copyright terms: Public domain | W3C validator |