Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpteq1i | Structured version Visualization version GIF version |
Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
mpteq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
mpteq1i | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | mpteq1 5157 | . 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 ↦ cmpt 5149 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-ral 3146 df-opab 5132 df-mpt 5150 |
This theorem is referenced by: fmptap 6935 mpompt 7269 offres 7687 mpomptsx 7765 mpompts 7766 pwfseq 10089 wrd2f1tovbij 14327 pmtrprfval 18618 gsum2dlem2 19094 gsumcom2 19098 srgbinomlem4 19296 ply1coe 20467 m2detleiblem3 21241 m2detleiblem4 21242 pmatcollpw3fi1lem1 21397 restco 21775 limcdif 24477 dfarea 25541 istrkg2ld 26249 wlknwwlksnbij 27669 wwlksnextbij 27683 clwlknf1oclwwlkn 27866 dfhnorm2 28902 trlset 37301 limsupequzmptlem 42015 sge0iunmptlemfi 42702 sge0iunmpt 42707 hoidmvlelem3 42886 smfmulc1 43078 smflimsuplem2 43102 |
Copyright terms: Public domain | W3C validator |