![]() |
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 3775, to prevent ambiguity. Theorem sbcel1g 4409 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 4402). Theorem sbccsb 4429 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 3890 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1533 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2099 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3775 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2705 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1534 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3892 csbeq1 3893 csbeq2 3895 csbeq2d 3896 cbvcsbw 3900 cbvcsb 3901 csbid 3903 csbcow 3905 csbco 3906 csbtt 3907 csbconstg 3909 csbgfi 3911 nfcsb1d 3913 nfcsbd 3916 nfcsbw 3917 csbie 3926 csbied 3928 csbie2g 3933 cbvralcsf 3935 cbvreucsf 3937 cbvrabcsf 3938 csbprc 4402 sbcel12 4404 sbceqg 4405 csbnestgfw 4415 csbnestgf 4420 csbvarg 4427 csbexg 5304 bj-csbsnlem 36375 bj-csbprc 36382 csbcom2fi 37595 |
Copyright terms: Public domain | W3C validator |