| 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 1910 | . 2 ⊢ (𝐴 = 𝐶 → ∀𝑥 𝐴 = 𝐶) | |
| 2 | mpteq12f 5230 | . 2 ⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | |
| 3 | 1, 2 | sylan 580 | 1 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∀wal 1538 = wceq 1540 ∀wral 3061 ↦ cmpt 5225 |
| 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-10 2141 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-opab 5206 df-mpt 5226 |
| This theorem is referenced by: mpteq1OLD 5236 mpteqb 7035 fmptcof 7150 mapxpen 9183 prodeq2w 15946 prdsdsval2 17529 prdsdsval3 17530 ablfac2 20109 mdetunilem9 22626 mdetmul 22629 xkocnv 23822 voliun 25589 itgeq1fOLD 25807 itgeq2 25813 iblcnlem 25824 bddiblnc 25877 esumeq2 34037 esumcvg 34087 dvtan 37677 |
| Copyright terms: Public domain | W3C validator |