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 3772, to prevent ambiguity. Theorem sbcel1g 4365 shows an example of how ambiguity could arise if we did not use distinguished brackets. When 𝐴 is a proper class, this evaluates to the empty set (see csbprc 4358). Theorem sbccsb 4385 recovers 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 3883 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1536 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2114 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3772 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2799 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1537 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3885 csbeq1 3886 csbeq2 3888 csbeq2d 3889 cbvcsbw 3893 cbvcsb 3894 csbid 3896 csbcow 3898 csbco 3899 csbtt 3900 csbgfi 3903 nfcsb1d 3905 nfcsbd 3908 nfcsbw 3909 csbie2g 3923 cbvralcsf 3925 cbvreucsf 3927 cbvrabcsf 3928 csbprc 4358 sbcel12 4360 sbceqg 4361 csbnestgfw 4371 csbnestgf 4376 csbvarg 4383 csbexg 5214 bj-csbsnlem 34223 bj-csbprc 34229 csbcom2fi 35421 |
Copyright terms: Public domain | W3C validator |