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 3402, to prevent ambiguity. Theorem sbcel1g 3939 shows an example of how ambiguity could arise if we didn't use distinguished brackets. Theorem sbccsb 3956 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 3499 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1474 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 1977 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3402 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2596 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1475 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3501 csbeq1 3502 csbeq2 3503 cbvcsb 3504 csbid 3507 csbco 3509 csbtt 3510 nfcsb1d 3513 nfcsbd 3516 csbie2g 3530 cbvralcsf 3531 cbvreucsf 3533 cbvrabcsf 3534 csbprc 3932 csbprcOLD 3933 sbcel12 3935 sbceqg 3936 csbeq2d 3943 csbnestgf 3948 csbvarg 3955 csbexg 4720 bj-csbsnlem 32090 bj-csbprc 32096 csbcom2fi 33104 csbgfi 33105 sbcel12gOLD 37775 |
Copyright terms: Public domain | W3C validator |