| 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 2738 | . . 3 ⊢ (⊤ → 𝐶 = 𝐶) | |
| 4 | 2, 3 | mpteq12dv 5233 | . 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶)) |
| 5 | 4 | mptru 1547 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ⊤wtru 1541 ↦ cmpt 5225 |
| 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 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-opab 5206 df-mpt 5226 |
| This theorem is referenced by: fmptap 7190 mpompt 7547 offres 8008 mpomptsx 8089 mpompts 8090 pwfseq 10704 wrd2f1tovbij 14999 pmtrprfval 19505 gsum2dlem2 19989 gsumcom2 19993 srgbinomlem4 20226 ply1coe 22302 m2detleiblem3 22635 m2detleiblem4 22636 pmatcollpw3fi1lem1 22792 restco 23172 limcdif 25911 dfarea 27003 nosupcbv 27747 noinfcbv 27762 istrkg2ld 28468 wlknwwlksnbij 29908 wwlksnextbij 29922 clwlknf1oclwwlkn 30103 dfhnorm2 31141 ccatws1f1o 32936 gsumwrd2dccat 33070 algextdeglem4 33761 algextdeglem5 33762 trlset 40163 limsupequzmptlem 45743 sge0iunmptlemfi 46428 sge0iunmpt 46433 hoidmvlelem3 46612 smfmulc1 46811 smflimsuplem2 46836 tposrescnv 48779 swapf1f1o 48981 precoffunc 49066 |
| Copyright terms: Public domain | W3C validator |