![]() |
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 2374. See cbvmptfg 5257 for a less restrictive version requiring more axioms. (Revised by GG, 17-Jan-2024.) |
Ref | Expression |
---|---|
cbvmptf.1 | ⊢ Ⅎ𝑥𝐴 |
cbvmptf.2 | ⊢ Ⅎ𝑦𝐴 |
cbvmptf.3 | ⊢ Ⅎ𝑦𝐵 |
cbvmptf.4 | ⊢ Ⅎ𝑥𝐶 |
cbvmptf.5 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbvmptf | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1911 | . . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) | |
2 | cbvmptf.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2894 | . . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴 |
4 | nfs1v 2153 | . . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 | |
5 | 3, 4 | nfan 1896 | . . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
6 | eleq1w 2821 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
7 | sbequ12 2248 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) | |
8 | 6, 7 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
9 | 1, 5, 8 | cbvopab1 5222 | . . 3 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
10 | cbvmptf.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2894 | . . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴 |
12 | cbvmptf.3 | . . . . . . 7 ⊢ Ⅎ𝑦𝐵 | |
13 | 12 | nfeq2 2920 | . . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵 |
14 | 13 | nfsbv 2328 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
15 | 11, 14 | nfan 1896 | . . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
16 | nfv 1911 | . . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) | |
17 | eleq1w 2821 | . . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
18 | sbequ 2080 | . . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵)) | |
19 | cbvmptf.4 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
20 | 19 | nfeq2 2920 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶 |
21 | cbvmptf.5 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
22 | 21 | eqeq2d 2745 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
23 | 20, 22 | sbiev 2312 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶) |
24 | 18, 23 | bitrdi 287 | . . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
25 | 17, 24 | anbi12d 632 | . . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
26 | 15, 16, 25 | cbvopab1 5222 | . . 3 ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
27 | 9, 26 | eqtri 2762 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
28 | df-mpt 5231 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
29 | df-mpt 5231 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
30 | 27, 28, 29 | 3eqtr4i 2772 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1536 [wsb 2061 ∈ wcel 2105 Ⅎwnfc 2887 {copab 5209 ↦ cmpt 5230 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-opab 5210 df-mpt 5231 |
This theorem is referenced by: cbvmpt 5258 resmptf 6058 fvmpt2f 7016 offval2f 7711 suppss2f 32654 fmptdF 32672 acunirnmpt2f 32677 funcnv4mpt 32685 cbvesum 34022 esumpfinvalf 34056 binomcxplemdvbinom 44348 binomcxplemdvsum 44350 binomcxplemnotnn0 44351 fmptff 45214 supxrleubrnmptf 45400 fnlimfv 45618 fnlimfvre2 45632 fnlimf 45633 limsupequzmptf 45686 sge0iunmptlemre 46370 smflim 46732 smflim2 46761 smfsup 46769 smfinf 46773 smflimsuplem2 46776 smflimsuplem5 46779 smflimsup 46783 smfliminf 46786 |
Copyright terms: Public domain | W3C validator |