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 1830 | . . . 4 ⊢ Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) | |
2 | nfv 1830 | . . . . 5 ⊢ Ⅎ𝑥 𝑤 ∈ 𝐴 | |
3 | nfs1v 2425 | . . . . 5 ⊢ Ⅎ𝑥[𝑤 / 𝑥]𝑧 = 𝐵 | |
4 | 2, 3 | nfan 1816 | . . . 4 ⊢ Ⅎ𝑥(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
5 | eleq1 2676 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑥 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴)) | |
6 | sbequ12 2097 | . . . . 5 ⊢ (𝑥 = 𝑤 → (𝑧 = 𝐵 ↔ [𝑤 / 𝑥]𝑧 = 𝐵)) | |
7 | 5, 6 | anbi12d 743 | . . . 4 ⊢ (𝑥 = 𝑤 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵))) |
8 | 1, 4, 7 | cbvopab1 4655 | . . 3 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} |
9 | nfv 1830 | . . . . 5 ⊢ Ⅎ𝑦 𝑤 ∈ 𝐴 | |
10 | cbvmpt.1 | . . . . . . 7 ⊢ Ⅎ𝑦𝐵 | |
11 | 10 | nfeq2 2766 | . . . . . 6 ⊢ Ⅎ𝑦 𝑧 = 𝐵 |
12 | 11 | nfsb 2428 | . . . . 5 ⊢ Ⅎ𝑦[𝑤 / 𝑥]𝑧 = 𝐵 |
13 | 9, 12 | nfan 1816 | . . . 4 ⊢ Ⅎ𝑦(𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) |
14 | nfv 1830 | . . . 4 ⊢ Ⅎ𝑤(𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶) | |
15 | eleq1 2676 | . . . . 5 ⊢ (𝑤 = 𝑦 → (𝑤 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
16 | sbequ 2364 | . . . . . 6 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ [𝑦 / 𝑥]𝑧 = 𝐵)) | |
17 | cbvmpt.2 | . . . . . . . 8 ⊢ Ⅎ𝑥𝐶 | |
18 | 17 | nfeq2 2766 | . . . . . . 7 ⊢ Ⅎ𝑥 𝑧 = 𝐶 |
19 | cbvmpt.3 | . . . . . . . 8 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
20 | 19 | eqeq2d 2620 | . . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
21 | 18, 20 | sbie 2396 | . . . . . 6 ⊢ ([𝑦 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶) |
22 | 16, 21 | syl6bb 275 | . . . . 5 ⊢ (𝑤 = 𝑦 → ([𝑤 / 𝑥]𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
23 | 15, 22 | anbi12d 743 | . . . 4 ⊢ (𝑤 = 𝑦 → ((𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
24 | 13, 14, 23 | cbvopab1 4655 | . . 3 ⊢ {〈𝑤, 𝑧〉 ∣ (𝑤 ∈ 𝐴 ∧ [𝑤 / 𝑥]𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
25 | 8, 24 | eqtri 2632 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
26 | df-mpt 4645 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
27 | df-mpt 4645 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
28 | 25, 26, 27 | 3eqtr4i 2642 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 [wsb 1867 ∈ wcel 1977 Ⅎwnfc 2738 {copab 4642 ↦ cmpt 4643 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-opab 4644 df-mpt 4645 |
This theorem is referenced by: cbvmptv 4678 dffn5f 6162 fvmpts 6194 fvmpt2i 6199 fvmptex 6203 fmptcof 6304 fmptcos 6305 fliftfuns 6464 offval2 6812 ofmpteq 6814 mpt2curryvald 7283 qliftfuns 7721 axcc2 9142 ac6num 9184 seqof2 12721 summolem2a 14293 zsum 14296 fsumcvg2 14305 fsumrlim 14384 cbvprod 14484 prodmolem2a 14503 zprod 14506 fprod 14510 pcmptdvds 15436 prdsdsval2 15967 gsumconstf 18158 gsummpt1n0 18187 gsum2d2 18196 dprd2d2 18266 gsumdixp 18432 psrass1lem 19198 coe1fzgsumdlem 19492 gsumply1eq 19496 evl1gsumdlem 19541 madugsum 20268 cnmpt1t 21278 cnmpt2k 21301 elmptrab 21440 flfcnp2 21621 prdsxmet 21984 fsumcn 22481 ovoliunlem3 23079 ovoliun 23080 ovoliun2 23081 voliun 23129 mbfpos 23224 mbfposb 23226 i1fposd 23280 itg2cnlem1 23334 isibl2 23339 cbvitg 23348 itgss3 23387 itgfsum 23399 itgabs 23407 itgcn 23415 limcmpt 23453 dvmptfsum 23542 lhop2 23582 dvfsumle 23588 dvfsumlem2 23594 itgsubstlem 23615 itgsubst 23616 itgulm2 23967 rlimcnp2 24493 gsummpt2co 29111 esumsnf 29453 mbfposadd 32627 itgabsnc 32649 ftc1cnnclem 32653 ftc2nc 32664 mzpsubst 36329 rabdiophlem2 36384 aomclem8 36649 fsumcnf 38203 disjf1 38364 disjrnmpt2 38370 disjinfi 38375 cncfmptss 38654 mulc1cncfg 38656 expcnfg 38658 fprodcn 38667 fnlimabslt 38746 icccncfext 38773 cncficcgt0 38774 cncfiooicclem1 38779 fprodcncf 38787 dvmptmulf 38827 iblsplitf 38862 stoweidlem21 38914 stirlinglem4 38970 stirlinglem13 38979 stirlinglem15 38981 fourierd 39115 fourierclimd 39116 sge0iunmptlemre 39308 sge0iunmpt 39311 sge0ltfirpmpt2 39319 sge0isummpt2 39325 sge0xaddlem2 39327 sge0xadd 39328 meadjiun 39359 omeiunle 39407 caratheodorylem2 39417 ovncvrrp 39454 vonioo 39573 |
Copyright terms: Public domain | W3C validator |