Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpteq12 | Structured version Visualization version GIF version |
Description: An equality theorem for the maps to notation. (Contributed by NM, 16-Dec-2013.) |
Ref | Expression |
---|---|
mpteq12 | ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-5 1827 | . 2 ⊢ (𝐴 = 𝐶 → ∀𝑥 𝐴 = 𝐶) | |
2 | mpteq12f 4661 | . 2 ⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | |
3 | 1, 2 | sylan 487 | 1 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∀wal 1473 = wceq 1475 ∀wral 2896 ↦ 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-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-ral 2901 df-opab 4644 df-mpt 4645 |
This theorem is referenced by: mpteq1 4665 mpteqb 6207 fmptcof 6304 mapxpen 8011 prodeq2w 14481 prdsdsval2 15967 prdsdsval3 15968 ablfac2 18311 mdetunilem9 20245 mdetmul 20248 xkocnv 21427 voliun 23129 itgeq1f 23344 itgeq2 23350 iblcnlem 23361 esumeq2 29425 esumcvg 29475 dvtan 32630 bddiblnc 32650 |
Copyright terms: Public domain | W3C validator |