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 2389. See cbvmptfg 5169 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 1914 | . . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) | |
2 | cbvmptf.1 | . . . . . 6 ⊢ Ⅎ𝑥𝐴 | |
3 | 2 | nfcri 2974 | . . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴 |
4 | nfs1v 2159 | . . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 | |
5 | 3, 4 | nfan 1899 | . . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
6 | eleq1w 2898 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
7 | sbequ12 2252 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) | |
8 | 6, 7 | anbi12d 632 | . . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
9 | 1, 5, 8 | cbvopab1 5142 | . . 3 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
10 | cbvmptf.2 | . . . . . 6 ⊢ Ⅎ𝑦𝐴 | |
11 | 10 | nfcri 2974 | . . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴 |
12 | cbvmptf.3 | . . . . . . 7 ⊢ Ⅎ𝑦𝐵 | |
13 | 12 | nfeq2 2998 | . . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵 |
14 | 13 | nfsbv 2348 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
15 | 11, 14 | nfan 1899 | . . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
16 | nfv 1914 | . . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) | |
17 | eleq1w 2898 | . . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
18 | sbequ 2089 | . . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵)) | |
19 | cbvmptf.4 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
20 | 19 | nfeq2 2998 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶 |
21 | cbvmptf.5 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
22 | 21 | eqeq2d 2835 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
23 | 20, 22 | sbiev 2329 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶) |
24 | 18, 23 | syl6bb 289 | . . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
25 | 17, 24 | anbi12d 632 | . . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
26 | 15, 16, 25 | cbvopab1 5142 | . . 3 ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
27 | 9, 26 | eqtri 2847 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
28 | df-mpt 5150 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
29 | df-mpt 5150 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
30 | 27, 28, 29 | 3eqtr4i 2857 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1536 [wsb 2068 ∈ wcel 2113 Ⅎwnfc 2964 {copab 5131 ↦ cmpt 5149 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-rab 3150 df-v 3499 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-nul 4295 df-if 4471 df-sn 4571 df-pr 4573 df-op 4577 df-opab 5132 df-mpt 5150 |
This theorem is referenced by: cbvmpt 5170 resmptf 5910 fvmpt2f 6772 offval2f 7424 suppss2f 30387 fmptdF 30404 acunirnmpt2f 30409 funcnv4mpt 30417 cbvesum 31305 esumpfinvalf 31339 binomcxplemdvbinom 40691 binomcxplemdvsum 40693 binomcxplemnotnn0 40694 supxrleubrnmptf 41733 fnlimfv 41950 fnlimfvre2 41964 fnlimf 41965 limsupequzmptf 42018 sge0iunmptlemre 42704 smflim 43060 smflim2 43087 smfsup 43095 smfinf 43099 smflimsuplem2 43102 smflimsuplem5 43105 smflimsup 43109 smfliminf 43112 |
Copyright terms: Public domain | W3C validator |