![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-csb | Structured version Visualization version GIF 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 3468, to prevent ambiguity. Theorem sbcel1g 4020 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 4037 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 setvar 𝑥 | |
2 | cA | . . 3 class 𝐴 | |
3 | cB | . . 3 class 𝐵 | |
4 | 1, 2, 3 | csb 3566 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1522 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2030 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3468 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2637 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1523 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3568 csbeq1 3569 csbeq2 3570 cbvcsb 3571 csbid 3574 csbco 3576 csbtt 3577 nfcsb1d 3580 nfcsbd 3583 csbie2g 3597 cbvralcsf 3598 cbvreucsf 3600 cbvrabcsf 3601 csbprc 4013 csbprcOLD 4014 sbcel12 4016 sbceqg 4017 csbeq2d 4024 csbnestgf 4029 csbvarg 4036 csbexg 4825 bj-csbsnlem 33023 bj-csbprc 33029 csbcom2fi 34064 csbgfi 34065 sbcel12gOLD 39071 |
Copyright terms: Public domain | W3C validator |