![]() |
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 3720, to prevent ambiguity. Theorem sbcel1g 4321 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 4313). Theorem sbccsb 4341 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 3828 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1537 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2111 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3720 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2776 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1538 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3830 csbeq1 3831 csbeq2 3833 csbeq2d 3834 cbvcsbw 3838 cbvcsb 3839 csbid 3841 csbcow 3843 csbco 3844 csbtt 3845 csbgfi 3848 nfcsb1d 3850 nfcsbd 3853 nfcsbw 3854 csbie2g 3868 cbvralcsf 3870 cbvreucsf 3872 cbvrabcsf 3873 csbprc 4313 csb0 4314 sbcel12 4316 sbceqg 4317 csbnestgfw 4327 csbnestgf 4332 csbvarg 4339 csbexg 5178 bj-csbsnlem 34344 bj-csbprc 34350 csbcom2fi 35566 |
Copyright terms: Public domain | W3C validator |