![]() |
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 2734 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | mpteq12dv 5240 | 1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ↦ cmpt 5232 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-opab 5212 df-mpt 5233 |
This theorem is referenced by: mpteq1d 5244 mpteq1iOLD 5246 tposf12 8236 oarec 8562 wunex2 10733 wuncval2 10742 vrmdfval 18737 pmtrfval 19318 sylow1 19471 sylow2b 19491 sylow3lem5 19499 sylow3 19501 gsumconst 19802 gsum2dlem2 19839 gsumfsum 21012 mvrfval 21540 mplcoe1 21592 mplcoe5 21595 evlsval 21649 coe1fzgsumd 21826 evls1fval 21838 evl1gsumd 21876 mavmul0 22054 madugsum 22145 cramer0 22192 cnmpt1t 23169 cnmpt2t 23177 fmval 23447 symgtgp 23610 prdstgpd 23629 gsumvsca1 32371 gsumvsca2 32372 qusima 32519 qusrn 32520 nsgmgc 32523 nsgqusf1olem2 32525 indv 33010 gsumesum 33057 esumlub 33058 esum2d 33091 sitg0 33345 matunitlindflem1 36484 matunitlindf 36486 sdclem2 36610 fsovcnvlem 42764 ntrneibex 42824 stoweidlem9 44725 sge0sn 45095 sge0iunmptlemfi 45129 sge0isum 45143 ovn02 45284 |
Copyright terms: Public domain | W3C validator |