![]() |
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 2733 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | mpteq12dv 5238 | 1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ↦ cmpt 5230 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-opab 5210 df-mpt 5231 |
This theorem is referenced by: mpteq1d 5242 mpteq1iOLD 5244 tposf12 8232 oarec 8558 wunex2 10729 wuncval2 10738 vrmdfval 18733 pmtrfval 19312 sylow1 19465 sylow2b 19485 sylow3lem5 19493 sylow3 19495 gsumconst 19796 gsum2dlem2 19833 gsumfsum 21004 mvrfval 21531 mplcoe1 21583 mplcoe5 21586 evlsval 21640 coe1fzgsumd 21817 evls1fval 21829 evl1gsumd 21867 mavmul0 22045 madugsum 22136 cramer0 22183 cnmpt1t 23160 cnmpt2t 23168 fmval 23438 symgtgp 23601 prdstgpd 23620 gsumvsca1 32358 gsumvsca2 32359 qusima 32507 qusrn 32508 nsgmgc 32511 nsgqusf1olem2 32513 indv 32998 gsumesum 33045 esumlub 33046 esum2d 33079 sitg0 33333 matunitlindflem1 36472 matunitlindf 36474 sdclem2 36598 fsovcnvlem 42749 ntrneibex 42809 stoweidlem9 44711 sge0sn 45081 sge0iunmptlemfi 45115 sge0isum 45129 ovn02 45270 |
Copyright terms: Public domain | W3C validator |