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 2740 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐶 = 𝐶) | |
2 | 1 | rgen 3064 | . 2 ⊢ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶 |
3 | mpteq12 5127 | . 2 ⊢ ((𝐴 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝐶 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | |
4 | 2, 3 | mpan2 691 | 1 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ∀wral 3054 ↦ cmpt 5120 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-12 2179 ax-ext 2711 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-ral 3059 df-opab 5103 df-mpt 5121 |
This theorem is referenced by: mpteq1d 5129 mpteq1i 5130 tposf12 7959 oarec 8232 wunex2 10251 wuncval2 10260 vrmdfval 18150 pmtrfval 18709 sylow1 18859 sylow2b 18879 sylow3lem5 18887 sylow3 18889 gsumconst 19186 gsum2dlem2 19223 gsumfsum 20297 mvrfval 20812 mplcoe1 20861 mplcoe5 20864 evlsval 20913 coe1fzgsumd 21090 evls1fval 21102 evl1gsumd 21140 mavmul0 21316 madugsum 21407 cramer0 21454 cnmpt1t 22429 cnmpt2t 22437 fmval 22707 symgtgp 22870 prdstgpd 22889 gsumvsca1 31069 gsumvsca2 31070 qusima 31179 nsgmgc 31182 nsgqusf1olem2 31184 indv 31563 gsumesum 31610 esumlub 31611 esum2d 31644 sitg0 31896 matunitlindflem1 35429 matunitlindf 35431 sdclem2 35556 fsovcnvlem 41208 ntrneibex 41270 stoweidlem9 43133 sge0sn 43500 sge0iunmptlemfi 43534 sge0isum 43548 ovn02 43689 |
Copyright terms: Public domain | W3C validator |