![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrabw | Structured version Visualization version GIF version |
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. Version of cbvrab 3438 with a disjoint variable condition, which does not require ax-13 2379. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Gino Giotto, 10-Jan-2024.) |
Ref | Expression |
---|---|
cbvrabw.1 | ⊢ Ⅎ𝑥𝐴 |
cbvrabw.2 | ⊢ Ⅎ𝑦𝐴 |
cbvrabw.3 | ⊢ Ⅎ𝑦𝜑 |
cbvrabw.4 | ⊢ Ⅎ𝑥𝜓 |
cbvrabw.5 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrabw | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝜑) | |
2 | cbvrabw.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2943 | . . . . 5 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | nfs1v 2157 | . . . . 5 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑 | |
5 | 3, 4 | nfan 1900 | . . . 4 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
6 | eleq1w 2872 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) | |
7 | sbequ12 2250 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) | |
8 | 6, 7 | anbi12d 633 | . . . 4 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑))) |
9 | 1, 5, 8 | cbvabw 2867 | . . 3 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} |
10 | cbvrabw.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2943 | . . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴 |
12 | cbvrabw.3 | . . . . . 6 ⊢ Ⅎ𝑦𝜑 | |
13 | 12 | nfsbv 2338 | . . . . 5 ⊢ Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
14 | 11, 13 | nfan 1900 | . . . 4 ⊢ Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
15 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧(𝑦 ∈ 𝐴 ∧ 𝜓) | |
16 | eleq1w 2872 | . . . . 5 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
17 | sbequ 2088 | . . . . . 6 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
18 | cbvrabw.4 | . . . . . . 7 ⊢ Ⅎ𝑥𝜓 | |
19 | cbvrabw.5 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
20 | 18, 19 | sbiev 2322 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
21 | 17, 20 | syl6bb 290 | . . . . 5 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | anbi12d 633 | . . . 4 ⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
23 | 14, 15, 22 | cbvabw 2867 | . . 3 ⊢ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
24 | 9, 23 | eqtri 2821 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
25 | df-rab 3115 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
26 | df-rab 3115 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} | |
27 | 24, 25, 26 | 3eqtr4i 2831 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 Ⅎwnf 1785 [wsb 2069 ∈ wcel 2111 {cab 2776 Ⅎwnfc 2936 {crab 3110 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-rab 3115 |
This theorem is referenced by: elrabsf 3764 f1ossf1o 6867 tfis 7549 cantnflem1 9136 scottexs 9300 scott0s 9301 elmptrab 22432 bnj1534 32235 scottexf 35606 scott0f 35607 eq0rabdioph 39717 rexrabdioph 39735 rexfrabdioph 39736 elnn0rabdioph 39744 dvdsrabdioph 39751 binomcxplemdvsum 41059 fnlimcnv 42309 fnlimabslt 42321 stoweidlem34 42676 stoweidlem59 42701 pimltmnf2 43336 pimgtpnf2 43342 pimltpnf2 43348 issmff 43368 smfpimltxrmpt 43392 smfpreimagtf 43401 smflim 43410 smfpimgtxr 43413 smfpimgtxrmpt 43417 smflim2 43437 smflimsup 43459 smfliminf 43462 |
Copyright terms: Public domain | W3C validator |