Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpteq12i | Structured version Visualization version GIF version |
Description: An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Ref | Expression |
---|---|
mpteq12i.1 | ⊢ 𝐴 = 𝐶 |
mpteq12i.2 | ⊢ 𝐵 = 𝐷 |
Ref | Expression |
---|---|
mpteq12i | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq12i.1 | . . . 4 ⊢ 𝐴 = 𝐶 | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → 𝐴 = 𝐶) |
3 | mpteq12i.2 | . . . 4 ⊢ 𝐵 = 𝐷 | |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → 𝐵 = 𝐷) |
5 | 2, 4 | mpteq12dv 4663 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) |
6 | 5 | trud 1484 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ⊤wtru 1476 ↦ 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: offres 7054 pmtrprfval 17730 evlsval 19340 madufval 20262 limcdif 23446 dfhnorm2 27363 cdj3lem3 28681 cdj3lem3b 28683 partfun 28858 esumsnf 29453 esumrnmpt2 29457 measinb2 29613 eulerpart 29771 fiblem 29787 trlset 34466 hoidmvlelem4 39488 |
Copyright terms: Public domain | W3C validator |