![]() |
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 2371. See cbvmptfg 5257 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 1917 | . . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) | |
2 | cbvmptf.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2890 | . . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴 |
4 | nfs1v 2153 | . . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 | |
5 | 3, 4 | nfan 1902 | . . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
6 | eleq1w 2816 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
7 | sbequ12 2243 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) | |
8 | 6, 7 | anbi12d 631 | . . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
9 | 1, 5, 8 | cbvopab1 5222 | . . 3 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
10 | cbvmptf.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2890 | . . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴 |
12 | cbvmptf.3 | . . . . . . 7 ⊢ Ⅎ𝑦𝐵 | |
13 | 12 | nfeq2 2920 | . . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵 |
14 | 13 | nfsbv 2323 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
15 | 11, 14 | nfan 1902 | . . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
16 | nfv 1917 | . . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) | |
17 | eleq1w 2816 | . . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
18 | sbequ 2086 | . . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵)) | |
19 | cbvmptf.4 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
20 | 19 | nfeq2 2920 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶 |
21 | cbvmptf.5 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
22 | 21 | eqeq2d 2743 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
23 | 20, 22 | sbiev 2308 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶) |
24 | 18, 23 | bitrdi 286 | . . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
25 | 17, 24 | anbi12d 631 | . . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
26 | 15, 16, 25 | cbvopab1 5222 | . . 3 ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
27 | 9, 26 | eqtri 2760 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
28 | df-mpt 5231 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
29 | df-mpt 5231 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
30 | 27, 28, 29 | 3eqtr4i 2770 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 [wsb 2067 ∈ wcel 2106 Ⅎwnfc 2883 {copab 5209 ↦ cmpt 5230 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-opab 5210 df-mpt 5231 |
This theorem is referenced by: cbvmpt 5258 resmptf 6037 fvmpt2f 6996 offval2f 7681 suppss2f 31850 fmptdF 31868 acunirnmpt2f 31873 funcnv4mpt 31881 cbvesum 33028 esumpfinvalf 33062 binomcxplemdvbinom 43097 binomcxplemdvsum 43099 binomcxplemnotnn0 43100 fmptff 43960 supxrleubrnmptf 44147 fnlimfv 44365 fnlimfvre2 44379 fnlimf 44380 limsupequzmptf 44433 sge0iunmptlemre 45117 smflim 45479 smflim2 45508 smfsup 45516 smfinf 45520 smflimsuplem2 45523 smflimsuplem5 45526 smflimsup 45530 smfliminf 45533 |
Copyright terms: Public domain | W3C validator |