Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpteq2da | Structured version Visualization version GIF version |
Description: Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) |
Ref | Expression |
---|---|
mpteq2da.1 | ⊢ Ⅎ𝑥𝜑 |
mpteq2da.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
mpteq2da | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2610 | . . 3 ⊢ 𝐴 = 𝐴 | |
2 | 1 | ax-gen 1713 | . 2 ⊢ ∀𝑥 𝐴 = 𝐴 |
3 | mpteq2da.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
4 | mpteq2da.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶) | |
5 | 4 | ex 449 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)) |
6 | 3, 5 | ralrimi 2940 | . 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) |
7 | mpteq12f 4661 | . 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) | |
8 | 2, 6, 7 | sylancr 694 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∀wal 1473 = wceq 1475 Ⅎwnf 1699 ∈ wcel 1977 ∀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: mpteq2dva 4672 offval2f 6807 prodeq1f 14477 prodeq2ii 14482 gsumsnfd 18174 gsummoncoe1 19495 cayleyhamilton1 20516 xkocnv 21427 utopsnneiplem 21861 fpwrelmap 28896 gsummpt2d 29112 esumf1o 29439 esum2d 29482 itg2addnclem 32631 ftc1anclem5 32659 mzpsubmpt 36324 mzpexpmpt 36326 refsum2cnlem1 38219 fmuldfeqlem1 38649 cncfiooicclem1 38779 dvmptfprodlem 38834 stoweidlem2 38895 stoweidlem6 38899 stoweidlem8 38901 stoweidlem17 38910 stoweidlem19 38912 stoweidlem20 38913 stoweidlem21 38914 stoweidlem22 38915 stoweidlem23 38916 stoweidlem32 38925 stoweidlem36 38929 stoweidlem40 38933 stoweidlem41 38934 stoweidlem47 38940 stirlinglem15 38981 sge0ss 39305 sge0xp 39322 omeiunlempt 39410 hoicvrrex 39446 ovnlecvr2 39500 smfdiv 39682 |
Copyright terms: Public domain | W3C validator |