| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbvmpov | Structured version Visualization version GIF version | ||
| Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5253, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.) |
| Ref | Expression |
|---|---|
| cbvmpov.1 | ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) |
| cbvmpov.2 | ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) |
| Ref | Expression |
|---|---|
| cbvmpov | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1w 2824 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) | |
| 2 | eleq1w 2824 | . . . . 5 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵)) | |
| 3 | 1, 2 | bi2anan9 638 | . . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵))) |
| 4 | cbvmpov.1 | . . . . . 6 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) | |
| 5 | cbvmpov.2 | . . . . . 6 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) | |
| 6 | 4, 5 | sylan9eq 2797 | . . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) |
| 7 | 6 | eqeq2d 2748 | . . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = 𝐶 ↔ 𝑣 = 𝐷)) |
| 8 | 3, 7 | anbi12d 632 | . . 3 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷))) |
| 9 | 8 | cbvoprab12v 7523 | . 2 ⊢ {〈〈𝑥, 𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)} |
| 10 | df-mpo 7436 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} | |
| 11 | df-mpo 7436 | . 2 ⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)} | |
| 12 | 9, 10, 11 | 3eqtr4i 2775 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 {coprab 7432 ∈ cmpo 7433 |
| 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-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-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 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-oprab 7435 df-mpo 7436 |
| This theorem is referenced by: fvproj 8159 seqomlem0 8489 dffi3 9471 cantnfsuc 9710 fin23lem33 10385 om2uzrdg 13997 uzrdgsuci 14001 sadcp1 16492 smupp1 16517 imasvscafn 17582 mgmnsgrpex 18944 sgrpnmndex 18945 sylow1 19621 sylow2b 19641 sylow3lem5 19649 sylow3 19651 efgmval 19730 efgtf 19740 funcrngcsetc 20640 funcrngcsetcALT 20641 funcringcsetc 20674 frlmphl 21801 pmatcollpw3lem 22789 mp2pm2mplem3 22814 txbas 23575 mpomulcn 24891 bcth 25363 opnmbl 25637 mbfimaopn 25691 mbfi1fseq 25756 om2noseqrdg 28310 noseqrdgsuc 28314 motplusg 28550 ttgval 28883 ttgvalOLD 28884 opsqrlem3 32161 elrgspnlem2 33247 fedgmul 33682 mdetpmtr12 33824 madjusmdetlem4 33829 dya2iocival 34275 sxbrsigalem5 34290 sxbrsigalem6 34291 eulerpart 34384 sseqp1 34397 cvmliftlem15 35303 cvmlift2 35321 opnmbllem0 37663 mblfinlem1 37664 mblfinlem2 37665 sdc 37751 tendoplcbv 40777 dvhvaddcbv 41091 dvhvscacbv 41100 fsovcnvlem 44026 ntrneibex 44086 ioorrnopn 46320 hoidmvle 46615 ovnhoi 46618 hoimbl 46646 smflimlem6 46791 lmod1zr 48410 functhinclem4 49096 |
| Copyright terms: Public domain | W3C validator |