![]() |
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.) Remove all disjoint variable conditions. (Revised by SN, 11-Nov-2024.) |
Ref | Expression |
---|---|
mpteq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
mpteq1i | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq1i.1 | . . . 4 ⊢ 𝐴 = 𝐵 | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → 𝐴 = 𝐵) |
3 | eqidd 2734 | . . 3 ⊢ (⊤ → 𝐶 = 𝐶) | |
4 | 2, 3 | mpteq12dv 5240 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
5 | 4 | mptru 1549 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ⊤wtru 1543 ↦ cmpt 5232 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-opab 5212 df-mpt 5233 |
This theorem is referenced by: fmptap 7168 mpompt 7522 offres 7970 mpomptsx 8050 mpompts 8051 pwfseq 10659 wrd2f1tovbij 14911 pmtrprfval 19355 gsum2dlem2 19839 gsumcom2 19843 srgbinomlem4 20052 ply1coe 21820 m2detleiblem3 22131 m2detleiblem4 22132 pmatcollpw3fi1lem1 22288 restco 22668 limcdif 25393 dfarea 26465 nosupcbv 27205 noinfcbv 27220 istrkg2ld 27711 wlknwwlksnbij 29142 wwlksnextbij 29156 clwlknf1oclwwlkn 29337 dfhnorm2 30375 algextdeglem1 32772 trlset 39032 limsupequzmptlem 44444 sge0iunmptlemfi 45129 sge0iunmpt 45134 hoidmvlelem3 45313 smfmulc1 45512 smflimsuplem2 45537 |
Copyright terms: Public domain | W3C validator |