![]() |
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 3474 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2372. (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 1918 | . . . 4 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝜑) | |
2 | cbvrabw.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2891 | . . . . 5 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | nfs1v 2154 | . . . . 5 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑 | |
5 | 3, 4 | nfan 1903 | . . . 4 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
6 | eleq1w 2817 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) | |
7 | sbequ12 2244 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) | |
8 | 6, 7 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑))) |
9 | 1, 5, 8 | cbvabw 2807 | . . 3 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} |
10 | cbvrabw.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2891 | . . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴 |
12 | cbvrabw.3 | . . . . . 6 ⊢ Ⅎ𝑦𝜑 | |
13 | 12 | nfsbv 2324 | . . . . 5 ⊢ Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
14 | 11, 13 | nfan 1903 | . . . 4 ⊢ Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
15 | nfv 1918 | . . . 4 ⊢ Ⅎ𝑧(𝑦 ∈ 𝐴 ∧ 𝜓) | |
16 | eleq1w 2817 | . . . . 5 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
17 | sbequ 2087 | . . . . . 6 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
18 | cbvrabw.4 | . . . . . . 7 ⊢ Ⅎ𝑥𝜓 | |
19 | cbvrabw.5 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
20 | 18, 19 | sbiev 2309 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
21 | 17, 20 | bitrdi 287 | . . . . 5 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | anbi12d 632 | . . . 4 ⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
23 | 14, 15, 22 | cbvabw 2807 | . . 3 ⊢ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
24 | 9, 23 | eqtri 2761 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
25 | df-rab 3434 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
26 | df-rab 3434 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} | |
27 | 24, 25, 26 | 3eqtr4i 2771 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 Ⅎwnf 1786 [wsb 2068 ∈ wcel 2107 {cab 2710 Ⅎwnfc 2884 {crab 3433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-rab 3434 |
This theorem is referenced by: elrabsf 3826 f1ossf1o 7126 tfis 7844 cantnflem1 9684 scottexs 9882 scott0s 9883 elmptrab 23331 bnj1534 33864 scottexf 37036 scott0f 37037 eq0rabdioph 41514 rexrabdioph 41532 rexfrabdioph 41533 elnn0rabdioph 41541 dvdsrabdioph 41548 binomcxplemdvsum 43114 fnlimcnv 44383 fnlimabslt 44395 stoweidlem34 44750 stoweidlem59 44775 pimltmnf2f 45413 pimgtpnf2f 45421 pimltpnf2f 45428 issmff 45450 smfpimltxrmptf 45474 smfpreimagtf 45484 smflim 45493 smfpimgtxr 45496 smfpimgtxrmptf 45500 smflim2 45522 smflimsup 45544 smfliminf 45547 |
Copyright terms: Public domain | W3C validator |