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.) |
Ref | Expression |
---|---|
mpteq1 | ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqidd 2822 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶) | |
2 | 1 | rgen 3148 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶 |
3 | mpteq12 5145 | . 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | |
4 | 2, 3 | mpan2 687 | 1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 ∀wral 3138 ↦ cmpt 5138 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-12 2167 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2800 df-cleq 2814 df-clel 2893 df-ral 3143 df-opab 5121 df-mpt 5139 |
This theorem is referenced by: mpteq1d 5147 mpteq1i 5148 tposf12 7908 oarec 8178 wunex2 10149 wuncval2 10158 vrmdfval 18011 pmtrfval 18509 sylow1 18659 sylow2b 18679 sylow3lem5 18687 sylow3 18689 gsumconst 18985 gsum2dlem2 19022 mvrfval 20130 mplcoe1 20176 mplcoe5 20179 evlsval 20229 coe1fzgsumd 20400 evls1fval 20412 evl1gsumd 20450 gsumfsum 20542 mavmul0 21091 madugsum 21182 cramer0 21229 cnmpt1t 22203 cnmpt2t 22211 fmval 22481 symgtgp 22639 prdstgpd 22662 gsumvsca1 30782 gsumvsca2 30783 indv 31171 gsumesum 31218 esumlub 31219 esum2d 31252 sitg0 31504 matunitlindflem1 34770 matunitlindf 34772 sdclem2 34900 fsovcnvlem 40239 ntrneibex 40303 stoweidlem9 42175 sge0sn 42542 sge0iunmptlemfi 42576 sge0isum 42590 ovn02 42731 |
Copyright terms: Public domain | W3C validator |