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 1918 | . 2 ⊢ (𝐴 = 𝐶 → ∀𝑥 𝐴 = 𝐶) | |
2 | mpteq12f 5123 | . 2 ⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | |
3 | 1, 2 | sylan 583 | 1 ⊢ ((𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ∀wal 1541 = wceq 1543 ∀wral 3051 ↦ cmpt 5120 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-12 2177 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-opab 5102 df-mpt 5121 |
This theorem is referenced by: mpteq1 5128 mpteqb 6815 fmptcof 6923 mapxpen 8790 prodeq2w 15437 prdsdsval2 16943 prdsdsval3 16944 ablfac2 19430 mdetunilem9 21471 mdetmul 21474 xkocnv 22665 voliun 24405 itgeq1f 24623 itgeq2 24629 iblcnlem 24640 bddiblnc 24693 esumeq2 31670 esumcvg 31720 dvtan 35513 |
Copyright terms: Public domain | W3C validator |