![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvmpt | 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.) |
Ref | Expression |
---|---|
cbvmpt.1 | ⊢ Ⅎ𝑦𝐵 |
cbvmpt.2 | ⊢ Ⅎ𝑥𝐶 |
cbvmpt.3 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbvmpt | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 2015 | . . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) | |
2 | nfv 2015 | . . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴 | |
3 | nfs1v 2313 | . . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 | |
4 | 2, 3 | nfan 2004 | . . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
5 | eleq1w 2888 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
6 | sbequ12 2288 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) | |
7 | 5, 6 | anbi12d 626 | . . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
8 | 1, 4, 7 | cbvopab1 4945 | . . 3 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
9 | nfv 2015 | . . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴 | |
10 | cbvmpt.1 | . . . . . . 7 ⊢ Ⅎ𝑦𝐵 | |
11 | 10 | nfeq2 2984 | . . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵 |
12 | 11 | nfsb 2574 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
13 | 9, 12 | nfan 2004 | . . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
14 | nfv 2015 | . . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) | |
15 | eleq1w 2888 | . . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
16 | sbequ 2506 | . . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵)) | |
17 | cbvmpt.2 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
18 | 17 | nfeq2 2984 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶 |
19 | cbvmpt.3 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
20 | 19 | eqeq2d 2834 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
21 | 18, 20 | sbie 2538 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶) |
22 | 16, 21 | syl6bb 279 | . . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
23 | 15, 22 | anbi12d 626 | . . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
24 | 13, 14, 23 | cbvopab1 4945 | . . 3 ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
25 | 8, 24 | eqtri 2848 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
26 | df-mpt 4952 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
27 | df-mpt 4952 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
28 | 25, 26, 27 | 3eqtr4i 2858 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1658 [wsb 2069 ∈ wcel 2166 Ⅎwnfc 2955 {copab 4934 ↦ cmpt 4951 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-rab 3125 df-v 3415 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-opab 4935 df-mpt 4952 |
This theorem is referenced by: cbvmptv 4972 dffn5f 6498 fvmpts 6531 fvmpt2i 6536 fvmptex 6540 fmptcof 6646 fmptcos 6647 fliftfuns 6818 offval2 7173 ofmpteq 7175 mpt2curryvald 7660 qliftfuns 8098 axcc2 9573 ac6num 9615 seqof2 13152 summolem2a 14822 zsum 14825 fsumcvg2 14834 fsumrlim 14916 cbvprod 15017 prodmolem2a 15036 zprod 15039 fprod 15043 pcmptdvds 15968 prdsdsval2 16496 gsumconstf 18687 gsummpt1n0 18716 gsum2d2 18725 dprd2d2 18796 gsumdixp 18962 psrass1lem 19737 coe1fzgsumdlem 20030 gsumply1eq 20034 evl1gsumdlem 20079 madugsum 20816 cnmpt1t 21838 cnmpt2k 21861 elmptrab 22000 flfcnp2 22180 prdsxmet 22543 fsumcn 23042 ovoliunlem3 23669 ovoliun 23670 ovoliun2 23671 voliun 23719 mbfpos 23816 mbfposb 23818 i1fposd 23872 itg2cnlem1 23926 isibl2 23931 cbvitg 23940 itgss3 23979 itgfsum 23991 itgabs 23999 itgcn 24007 limcmpt 24045 dvmptfsum 24136 lhop2 24176 dvfsumle 24182 dvfsumlem2 24188 itgsubstlem 24209 itgsubst 24210 itgulm2 24561 rlimcnp2 25105 gsummpt2co 30324 esumsnf 30670 mbfposadd 33999 itgabsnc 34021 ftc1cnnclem 34025 ftc2nc 34036 mzpsubst 38154 rabdiophlem2 38209 aomclem8 38473 fsumcnf 39997 disjf1 40176 disjrnmpt2 40182 disjinfi 40187 fmptf 40248 cncfmptss 40613 mulc1cncfg 40615 expcnfg 40617 fprodcn 40626 fnlimabslt 40705 climmptf 40707 liminfvalxr 40809 icccncfext 40894 cncficcgt0 40895 cncfiooicclem1 40900 fprodcncf 40908 dvmptmulf 40946 iblsplitf 40979 stoweidlem21 41031 stirlinglem4 41087 stirlinglem13 41096 stirlinglem15 41098 fourierd 41232 fourierclimd 41233 sge0iunmptlemre 41422 sge0iunmpt 41425 sge0ltfirpmpt2 41433 sge0isummpt2 41439 sge0xaddlem2 41441 sge0xadd 41442 meadjiun 41473 meaiunincf 41490 meaiuninc3 41492 omeiunle 41524 caratheodorylem2 41534 ovncvrrp 41571 vonioo 41689 smflim2 41805 smfsup 41813 smfinf 41817 smflimsup 41827 smfliminf 41830 |
Copyright terms: Public domain | W3C validator |