![]() |
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 3471 with a disjoint variable condition, which does not require ax-13 2369. (Contributed by Andrew Salmon, 11-Jul-2011.) Avoid ax-13 2369. (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 2888 | . . . . 5 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐴 |
4 | nfs1v 2151 | . . . . 5 ⊢ Ⅎ𝑥[𝑧 / 𝑥]𝜑 | |
5 | 3, 4 | nfan 1900 | . . . 4 ⊢ Ⅎ𝑥(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
6 | eleq1w 2814 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) | |
7 | sbequ12 2241 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) | |
8 | 6, 7 | anbi12d 629 | . . . 4 ⊢ (𝑥 = 𝑧 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑))) |
9 | 1, 5, 8 | cbvabw 2804 | . . 3 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} |
10 | cbvrabw.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2888 | . . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴 |
12 | cbvrabw.3 | . . . . . 6 ⊢ Ⅎ𝑦𝜑 | |
13 | 12 | nfsbv 2321 | . . . . 5 ⊢ Ⅎ𝑦[𝑧 / 𝑥]𝜑 |
14 | 11, 13 | nfan 1900 | . . . 4 ⊢ Ⅎ𝑦(𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) |
15 | nfv 1915 | . . . 4 ⊢ Ⅎ𝑧(𝑦 ∈ 𝐴 ∧ 𝜓) | |
16 | eleq1w 2814 | . . . . 5 ⊢ (𝑧 = 𝑦 → (𝑧 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
17 | sbequ 2084 | . . . . . 6 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)) | |
18 | cbvrabw.4 | . . . . . . 7 ⊢ Ⅎ𝑥𝜓 | |
19 | cbvrabw.5 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
20 | 18, 19 | sbiev 2306 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
21 | 17, 20 | bitrdi 286 | . . . . 5 ⊢ (𝑧 = 𝑦 → ([𝑧 / 𝑥]𝜑 ↔ 𝜓)) |
22 | 16, 21 | anbi12d 629 | . . . 4 ⊢ (𝑧 = 𝑦 → ((𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓))) |
23 | 14, 15, 22 | cbvabw 2804 | . . 3 ⊢ {𝑧 ∣ (𝑧 ∈ 𝐴 ∧ [𝑧 / 𝑥]𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
24 | 9, 23 | eqtri 2758 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} |
25 | df-rab 3431 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
26 | df-rab 3431 | . 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)} | |
27 | 24, 25, 26 | 3eqtr4i 2768 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1539 Ⅎwnf 1783 [wsb 2065 ∈ wcel 2104 {cab 2707 Ⅎwnfc 2881 {crab 3430 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-tru 1542 df-ex 1780 df-nf 1784 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-rab 3431 |
This theorem is referenced by: elrabsf 3824 f1ossf1o 7127 tfis 7846 cantnflem1 9686 scottexs 9884 scott0s 9885 elmptrab 23551 bnj1534 34162 scottexf 37339 scott0f 37340 eq0rabdioph 41816 rexrabdioph 41834 rexfrabdioph 41835 elnn0rabdioph 41843 dvdsrabdioph 41850 binomcxplemdvsum 43416 fnlimcnv 44681 fnlimabslt 44693 stoweidlem34 45048 stoweidlem59 45073 pimltmnf2f 45711 pimgtpnf2f 45719 pimltpnf2f 45726 issmff 45748 smfpimltxrmptf 45772 smfpreimagtf 45782 smflim 45791 smfpimgtxr 45794 smfpimgtxrmptf 45798 smflim2 45820 smflimsup 45842 smfliminf 45845 |
Copyright terms: Public domain | W3C validator |