| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > mpteq1 | Structured version Visualization version GIF version | ||
| Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.) |
| Ref | Expression |
|---|---|
| mpteq1 | ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
| 2 | eqidd 2738 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
| 3 | 1, 2 | mpteq12dv 5233 | 1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ↦ 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-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5206 df-mpt 5226 |
| This theorem is referenced by: mpteq1d 5237 mpteq1iOLD 5239 tposf12 8276 oarec 8600 wunex2 10778 wuncval2 10787 vrmdfval 18869 pmtrfval 19468 sylow1 19621 sylow2b 19641 sylow3lem5 19649 sylow3 19651 gsumconst 19952 gsum2dlem2 19989 gsumfsum 21452 mvrfval 22001 mplcoe1 22055 mplcoe5 22058 evlsval 22110 coe1fzgsumd 22308 evls1fval 22323 evl1gsumd 22361 mavmul0 22558 madugsum 22649 cramer0 22696 cnmpt1t 23673 cnmpt2t 23681 fmval 23951 symgtgp 24114 prdstgpd 24133 indv 32837 gsumvsca1 33232 gsumvsca2 33233 qusima 33436 qusrn 33437 nsgmgc 33440 nsgqusf1olem2 33442 gsumesum 34060 esumlub 34061 esum2d 34094 sitg0 34348 matunitlindflem1 37623 matunitlindf 37625 sdclem2 37749 evl1gprodd 42118 idomnnzgmulnz 42134 deg1gprod 42141 fsovcnvlem 44026 ntrneibex 44086 stoweidlem9 46024 sge0sn 46394 sge0iunmptlemfi 46428 sge0isum 46442 ovn02 46583 |
| Copyright terms: Public domain | W3C validator |