| 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 2377. See cbvmptfg 5252 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 1914 | . . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) | |
| 2 | cbvmptf.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
| 3 | 2 | nfcri 2897 | . . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴 |
| 4 | nfs1v 2156 | . . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 | |
| 5 | 3, 4 | nfan 1899 | . . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
| 6 | eleq1w 2824 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
| 7 | sbequ12 2251 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) | |
| 8 | 6, 7 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
| 9 | 1, 5, 8 | cbvopab1 5217 | . . 3 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
| 10 | cbvmptf.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
| 11 | 10 | nfcri 2897 | . . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴 |
| 12 | cbvmptf.3 | . . . . . . 7 ⊢ Ⅎ𝑦𝐵 | |
| 13 | 12 | nfeq2 2923 | . . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵 |
| 14 | 13 | nfsbv 2330 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
| 15 | 11, 14 | nfan 1899 | . . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
| 16 | nfv 1914 | . . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) | |
| 17 | eleq1w 2824 | . . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
| 18 | sbequ 2083 | . . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵)) | |
| 19 | cbvmptf.4 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
| 20 | 19 | nfeq2 2923 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶 |
| 21 | cbvmptf.5 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
| 22 | 21 | eqeq2d 2748 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
| 23 | 20, 22 | sbiev 2314 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶) |
| 24 | 18, 23 | bitrdi 287 | . . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
| 25 | 17, 24 | anbi12d 632 | . . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
| 26 | 15, 16, 25 | cbvopab1 5217 | . . 3 ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
| 27 | 9, 26 | eqtri 2765 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
| 28 | df-mpt 5226 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
| 29 | df-mpt 5226 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
| 30 | 27, 28, 29 | 3eqtr4i 2775 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 [wsb 2064 ∈ wcel 2108 Ⅎwnfc 2890 {copab 5205 ↦ cmpt 5225 |
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-opab 5206 df-mpt 5226 |
| This theorem is referenced by: cbvmpt 5253 resmptf 6057 fvmpt2f 7017 offval2f 7712 suppss2f 32648 fmptdF 32666 acunirnmpt2f 32671 funcnv4mpt 32679 cbvesum 34043 esumpfinvalf 34077 binomcxplemdvbinom 44372 binomcxplemdvsum 44374 binomcxplemnotnn0 44375 fmptff 45276 supxrleubrnmptf 45462 fnlimfv 45678 fnlimfvre2 45692 fnlimf 45693 limsupequzmptf 45746 sge0iunmptlemre 46430 smflim 46792 smflim2 46821 smfsup 46829 smfinf 46833 smflimsuplem2 46836 smflimsuplem5 46839 smflimsup 46843 smfliminf 46846 |
| Copyright terms: Public domain | W3C validator |