Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mptresid | Structured version Visualization version GIF version |
Description: The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.) |
Ref | Expression |
---|---|
mptresid | ⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opabresid 5960 | . 2 ⊢ ( I ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} | |
2 | df-mpt 5159 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} | |
3 | 1, 2 | eqtr4i 2770 | 1 ⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1539 ∈ wcel 2107 {copab 5137 ↦ cmpt 5158 I cid 5489 ↾ cres 5592 |
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-10 2138 ax-12 2172 ax-ext 2710 ax-sep 5224 ax-nul 5231 ax-pr 5353 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-rab 3074 df-v 3435 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-nul 4258 df-if 4461 df-sn 4563 df-pr 4565 df-op 4569 df-opab 5138 df-mpt 5159 df-id 5490 df-xp 5596 df-rel 5597 df-res 5602 |
This theorem is referenced by: idref 7027 2fvcoidd 7178 pwfseqlem5 10428 restid2 17150 curf2ndf 17974 hofcl 17986 yonedainv 18008 smndex2dlinvh 18565 sylow1lem2 19213 sylow3lem1 19241 0frgp 19394 frgpcyg 20790 evpmodpmf1o 20810 cnmptid 22821 txswaphmeolem 22964 idnghm 23916 dvexp 25126 dvmptid 25130 mvth 25165 plyid 25379 coeidp 25433 dgrid 25434 plyremlem 25473 taylply2 25536 wilthlem2 26227 ftalem7 26237 fusgrfis 27706 fzto1st1 31378 cycpm2tr 31395 zrhre 31978 qqhre 31979 fsovcnvlem 41628 fourierdlem60 43714 fourierdlem61 43715 itcoval0mpt 46023 |
Copyright terms: Public domain | W3C validator |