![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mptresid | Structured version Visualization version GIF version |
Description: The restricted identity expressed with the maps-to notation. (Contributed by FL, 25-Apr-2012.) |
Ref | Expression |
---|---|
mptresid | ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = ( I ↾ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-mpt 4954 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} | |
2 | opabresid 5699 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} = ( I ↾ 𝐴) | |
3 | 1, 2 | eqtri 2850 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = ( I ↾ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 386 = wceq 1658 ∈ wcel 2166 {copab 4936 ↦ cmpt 4953 I cid 5250 ↾ cres 5345 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-opab 4937 df-mpt 4954 df-id 5251 df-xp 5349 df-rel 5350 df-res 5355 |
This theorem is referenced by: idref 6663 2fvcoidd 6808 pwfseqlem5 9801 restid2 16445 curf2ndf 17241 hofcl 17253 yonedainv 17275 sylow1lem2 18366 sylow3lem1 18394 0frgp 18546 frgpcyg 20282 evpmodpmf1o 20303 txswaphmeolem 21979 idnghm 22918 dvexp 24116 dvmptid 24120 mvth 24155 plyid 24365 coeidp 24419 dgrid 24420 plyremlem 24459 taylply2 24522 wilthlem2 25209 ftalem7 25219 fusgrfis 26628 fzto1st1 30398 zrhre 30609 qqhre 30610 fsovcnvlem 39148 fourierdlem60 41178 fourierdlem61 41179 |
Copyright terms: Public domain | W3C validator |