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 2739 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | mpteq12dv 5165 | 1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ↦ cmpt 5157 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-opab 5137 df-mpt 5158 |
This theorem is referenced by: mpteq1d 5169 mpteq1iOLD 5171 tposf12 8067 oarec 8393 wunex2 10494 wuncval2 10503 vrmdfval 18495 pmtrfval 19058 sylow1 19208 sylow2b 19228 sylow3lem5 19236 sylow3 19238 gsumconst 19535 gsum2dlem2 19572 gsumfsum 20665 mvrfval 21189 mplcoe1 21238 mplcoe5 21241 evlsval 21296 coe1fzgsumd 21473 evls1fval 21485 evl1gsumd 21523 mavmul0 21701 madugsum 21792 cramer0 21839 cnmpt1t 22816 cnmpt2t 22824 fmval 23094 symgtgp 23257 prdstgpd 23276 gsumvsca1 31479 gsumvsca2 31480 qusima 31594 nsgmgc 31597 nsgqusf1olem2 31599 indv 31980 gsumesum 32027 esumlub 32028 esum2d 32061 sitg0 32313 matunitlindflem1 35773 matunitlindf 35775 sdclem2 35900 fsovcnvlem 41621 ntrneibex 41683 stoweidlem9 43550 sge0sn 43917 sge0iunmptlemfi 43951 sge0isum 43965 ovn02 44106 |
Copyright terms: Public domain | W3C validator |