|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > cbvmpo | Structured version Visualization version GIF version | ||
| Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by NM, 17-Dec-2013.) | 
| Ref | Expression | 
|---|---|
| cbvmpo.1 | ⊢ Ⅎ𝑧𝐶 | 
| cbvmpo.2 | ⊢ Ⅎ𝑤𝐶 | 
| cbvmpo.3 | ⊢ Ⅎ𝑥𝐷 | 
| cbvmpo.4 | ⊢ Ⅎ𝑦𝐷 | 
| cbvmpo.5 | ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) | 
| Ref | Expression | 
|---|---|
| cbvmpo | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | nfcv 2904 | . 2 ⊢ Ⅎ𝑧𝐵 | |
| 2 | nfcv 2904 | . 2 ⊢ Ⅎ𝑥𝐵 | |
| 3 | cbvmpo.1 | . 2 ⊢ Ⅎ𝑧𝐶 | |
| 4 | cbvmpo.2 | . 2 ⊢ Ⅎ𝑤𝐶 | |
| 5 | cbvmpo.3 | . 2 ⊢ Ⅎ𝑥𝐷 | |
| 6 | cbvmpo.4 | . 2 ⊢ Ⅎ𝑦𝐷 | |
| 7 | eqidd 2737 | . 2 ⊢ (𝑥 = 𝑧 → 𝐵 = 𝐵) | |
| 8 | cbvmpo.5 | . 2 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) | |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | cbvmpox 7527 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1539 Ⅎwnfc 2889 ∈ cmpo 7434 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-rab 3436 df-v 3481 df-dif 3953 df-un 3955 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-opab 5205 df-oprab 7436 df-mpo 7437 | 
| This theorem is referenced by: fvmpopr2d 7596 el2mpocsbcl 8111 fnmpoovd 8113 fmpoco 8121 mpocurryd 8295 fvmpocurryd 8297 xpf1o 9180 cnfcomlem 9740 fseqenlem1 10065 relexpsucnnr 15065 gsumdixp 20317 evlslem4 22101 madugsum 22650 cnmpt2t 23682 cnmptk2 23695 fmucnd 24302 fsum2cn 24896 aks6d1c7lem3 42184 fmpocos 42275 fmuldfeqlem1 45602 smflim 46797 | 
| Copyright terms: Public domain | W3C validator |