![]() |
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 3778, to prevent ambiguity. Theorem sbcel1g 4414 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 4407). Theorem sbccsb 4434 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 3894 | . 2 class ⦋𝐴 / 𝑥⦌𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1541 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2107 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wsbc 3778 | . . 3 wff [𝐴 / 𝑥]𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2710 | . 2 class {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1542 | 1 wff ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: csb2 3896 csbeq1 3897 csbeq2 3899 csbeq2d 3900 cbvcsbw 3904 cbvcsb 3905 csbid 3907 csbcow 3909 csbco 3910 csbtt 3911 csbconstg 3913 csbgfi 3915 nfcsb1d 3917 nfcsbd 3920 nfcsbw 3921 csbie 3930 csbied 3932 csbie2g 3937 cbvralcsf 3939 cbvreucsf 3941 cbvrabcsf 3942 csbprc 4407 sbcel12 4409 sbceqg 4410 csbnestgfw 4420 csbnestgf 4425 csbvarg 4432 csbexg 5311 bj-csbsnlem 35783 bj-csbprc 35790 csbcom2fi 36996 |
Copyright terms: Public domain | W3C validator |