![]() |
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 1980 | . 2 ⊢ (𝐴 = 𝐶 → ∀𝑥 𝐴 = 𝐶) | |
2 | mpteq12f 4875 | . 2 ⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | |
3 | 1, 2 | sylan 489 | 1 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∀wal 1622 = wceq 1624 ∀wral 3042 ↦ cmpt 4873 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-clab 2739 df-cleq 2745 df-clel 2748 df-ral 3047 df-opab 4857 df-mpt 4874 |
This theorem is referenced by: mpteq1 4881 mpteqb 6453 fmptcof 6552 mapxpen 8283 prodeq2w 14833 prdsdsval2 16338 prdsdsval3 16339 ablfac2 18680 mdetunilem9 20620 mdetmul 20623 xkocnv 21811 voliun 23514 itgeq1f 23729 itgeq2 23735 iblcnlem 23746 esumeq2 30399 esumcvg 30449 dvtan 33765 bddiblnc 33785 |
Copyright terms: Public domain | W3C validator |