Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvmptf | Structured version Visualization version GIF version |
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) (Revised by Thierry Arnoux, 9-Mar-2017.) Add disjoint variable condition to avoid ax-13 2373. See cbvmptfg 5185 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.) |
Ref | Expression |
---|---|
cbvmptf.1 | ⊢ Ⅎ𝑥𝐴 |
cbvmptf.2 | ⊢ Ⅎ𝑦𝐴 |
cbvmptf.3 | ⊢ Ⅎ𝑦𝐵 |
cbvmptf.4 | ⊢ Ⅎ𝑥𝐶 |
cbvmptf.5 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbvmptf | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1918 | . . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) | |
2 | cbvmptf.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2895 | . . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴 |
4 | nfs1v 2154 | . . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 | |
5 | 3, 4 | nfan 1903 | . . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
6 | eleq1w 2822 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
7 | sbequ12 2245 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) | |
8 | 6, 7 | anbi12d 631 | . . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
9 | 1, 5, 8 | cbvopab1 5150 | . . 3 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
10 | cbvmptf.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2895 | . . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴 |
12 | cbvmptf.3 | . . . . . . 7 ⊢ Ⅎ𝑦𝐵 | |
13 | 12 | nfeq2 2925 | . . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵 |
14 | 13 | nfsbv 2325 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
15 | 11, 14 | nfan 1903 | . . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
16 | nfv 1918 | . . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) | |
17 | eleq1w 2822 | . . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
18 | sbequ 2087 | . . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵)) | |
19 | cbvmptf.4 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
20 | 19 | nfeq2 2925 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶 |
21 | cbvmptf.5 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
22 | 21 | eqeq2d 2750 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
23 | 20, 22 | sbiev 2310 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶) |
24 | 18, 23 | bitrdi 287 | . . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
25 | 17, 24 | anbi12d 631 | . . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
26 | 15, 16, 25 | cbvopab1 5150 | . . 3 ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
27 | 9, 26 | eqtri 2767 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
28 | df-mpt 5159 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
29 | df-mpt 5159 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
30 | 27, 28, 29 | 3eqtr4i 2777 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1539 [wsb 2068 ∈ wcel 2107 Ⅎwnfc 2888 {copab 5137 ↦ cmpt 5158 |
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 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-opab 5138 df-mpt 5159 |
This theorem is referenced by: cbvmpt 5186 resmptf 5950 fvmpt2f 6885 offval2f 7557 suppss2f 30983 fmptdF 31002 acunirnmpt2f 31007 funcnv4mpt 31015 cbvesum 32019 esumpfinvalf 32053 binomcxplemdvbinom 41978 binomcxplemdvsum 41980 binomcxplemnotnn0 41981 supxrleubrnmptf 42998 fnlimfv 43211 fnlimfvre2 43225 fnlimf 43226 limsupequzmptf 43279 sge0iunmptlemre 43960 smflim 44322 smflim2 44350 smfsup 44358 smfinf 44362 smflimsuplem2 44365 smflimsuplem5 44368 smflimsup 44372 smfliminf 44375 |
Copyright terms: Public domain | W3C validator |