![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvrab | Structured version Visualization version GIF version |
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.) |
Ref | Expression |
---|---|
cbvrab.1 | ⊢ Ⅎ𝑥𝐴 |
cbvrab.2 | ⊢ Ⅎ𝑦𝐴 |
cbvrab.3 | ⊢ Ⅎ𝑦𝜑 |
cbvrab.4 | ⊢ Ⅎ𝑥𝜓 |
cbvrab.5 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
cbvrab | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1883 | . . . 4 ⊢ Ⅎ𝑧(𝑥 ∈ 𝐴 ∧ 𝜑) | |
2 | cbvrab.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2787 | . . . . 5 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | nfs1v 2465 | . . . . 5 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑 | |
5 | 3, 4 | nfan 1868 | . . . 4 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
6 | eleq1 2718 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) | |
7 | sbequ12 2149 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) | |
8 | 6, 7 | anbi12d 747 | . . . 4 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑))) |
9 | 1, 5, 8 | cbvab 2775 | . . 3 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} |
10 | cbvrab.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2787 | . . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴 |
12 | cbvrab.3 | . . . . . 6 ⊢ Ⅎ𝑦𝜑 | |
13 | 12 | nfsb 2468 | . . . . 5 ⊢ Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
14 | 11, 13 | nfan 1868 | . . . 4 ⊢ Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
15 | nfv 1883 | . . . 4 ⊢ Ⅎ𝑧(𝑦 ∈ 𝐴 ∧ 𝜓) | |
16 | eleq1 2718 | . . . . 5 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
17 | sbequ 2404 | . . . . . 6 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
18 | cbvrab.4 | . . . . . . 7 ⊢ Ⅎ𝑥𝜓 | |
19 | cbvrab.5 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
20 | 18, 19 | sbie 2436 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
21 | 17, 20 | syl6bb 276 | . . . . 5 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | anbi12d 747 | . . . 4 ⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
23 | 14, 15, 22 | cbvab 2775 | . . 3 ⊢ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
24 | 9, 23 | eqtri 2673 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
25 | df-rab 2950 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
26 | df-rab 2950 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} | |
27 | 24, 25, 26 | 3eqtr4i 2683 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1523 Ⅎwnf 1748 [wsb 1937 ∈ wcel 2030 {cab 2637 Ⅎwnfc 2780 {crab 2945 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rab 2950 |
This theorem is referenced by: cbvrabv 3230 elrabsf 3507 tfis 7096 cantnflem1 8624 scottexs 8788 scott0s 8789 elmptrab 21678 bnj1534 31049 scottexf 34106 scott0f 34107 eq0rabdioph 37657 rexrabdioph 37675 rexfrabdioph 37676 elnn0rabdioph 37684 dvdsrabdioph 37691 binomcxplemdvsum 38871 fnlimcnv 40217 fnlimabslt 40229 stoweidlem34 40569 stoweidlem59 40594 pimltmnf2 41232 pimgtpnf2 41238 pimltpnf2 41244 issmff 41264 smfpimltxrmpt 41288 smfpreimagtf 41297 smflim 41306 smfpimgtxr 41309 smfpimgtxrmpt 41313 smflim2 41333 smflimsup 41355 smfliminf 41358 |
Copyright terms: Public domain | W3C validator |