![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > csbab | Structured version Visualization version GIF version |
Description: Move substitution into a class abstraction. (Contributed by NM, 13-Dec-2005.) (Revised by NM, 19-Aug-2018.) |
Ref | Expression |
---|---|
csbab | ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-clab 2710 | . . . 4 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑) | |
2 | sbsbc 3780 | . . . 4 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑) | |
3 | 1, 2 | bitri 274 | . . 3 ⊢ (𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑} ↔ [𝑧 / 𝑦][𝐴 / 𝑥]𝜑) |
4 | sbccom 3864 | . . . 4 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑) | |
5 | df-clab 2710 | . . . . . 6 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝑧 / 𝑦]𝜑) | |
6 | sbsbc 3780 | . . . . . 6 ⊢ ([𝑧 / 𝑦]𝜑 ↔ [𝑧 / 𝑦]𝜑) | |
7 | 5, 6 | bitri 274 | . . . . 5 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝑧 / 𝑦]𝜑) |
8 | 7 | sbcbii 3836 | . . . 4 ⊢ ([𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑} ↔ [𝐴 / 𝑥][𝑧 / 𝑦]𝜑) |
9 | 4, 8 | bitr4i 277 | . . 3 ⊢ ([𝑧 / 𝑦][𝐴 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑}) |
10 | sbcel2 4414 | . . 3 ⊢ ([𝐴 / 𝑥]𝑧 ∈ {𝑦 ∣ 𝜑} ↔ 𝑧 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑}) | |
11 | 3, 9, 10 | 3bitrri 297 | . 2 ⊢ (𝑧 ∈ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ [𝐴 / 𝑥]𝜑}) |
12 | 11 | eqriv 2729 | 1 ⊢ ⦋𝐴 / 𝑥⦌{𝑦 ∣ 𝜑} = {𝑦 ∣ [𝐴 / 𝑥]𝜑} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 [wsb 2067 ∈ wcel 2106 {cab 2709 [wsbc 3776 ⦋csb 3892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-nul 4322 |
This theorem is referenced by: csbsng 4711 csbuni 4939 csbxp 5773 csbdm 5895 csbfrecsg 8265 csbwrdg 14490 abfmpeld 31866 abfmpel 31867 csboprabg 36199 csbfinxpg 36257 csbingVD 43630 csbsngVD 43639 csbxpgVD 43640 csbrngVD 43642 csbunigVD 43644 csbfv12gALTVD 43645 |
Copyright terms: Public domain | W3C validator |