![]() |
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 2735 | . . 3 ⊢ (⊤ → 𝐶 = 𝐶) | |
4 | 2, 3 | mpteq12dv 5238 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
5 | 4 | mptru 1543 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 ⊤wtru 1537 ↦ cmpt 5230 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-opab 5210 df-mpt 5231 |
This theorem is referenced by: fmptap 7189 mpompt 7546 offres 8006 mpomptsx 8087 mpompts 8088 pwfseq 10701 wrd2f1tovbij 14995 pmtrprfval 19519 gsum2dlem2 20003 gsumcom2 20007 srgbinomlem4 20246 ply1coe 22317 m2detleiblem3 22650 m2detleiblem4 22651 pmatcollpw3fi1lem1 22807 restco 23187 limcdif 25925 dfarea 27017 nosupcbv 27761 noinfcbv 27776 istrkg2ld 28482 wlknwwlksnbij 29917 wwlksnextbij 29931 clwlknf1oclwwlkn 30112 dfhnorm2 31150 ccatws1f1o 32920 gsumwrd2dccat 33052 algextdeglem4 33725 algextdeglem5 33726 trlset 40143 limsupequzmptlem 45683 sge0iunmptlemfi 46368 sge0iunmpt 46373 hoidmvlelem3 46552 smfmulc1 46751 smflimsuplem2 46776 |
Copyright terms: Public domain | W3C validator |