![]() |
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 6049 | . 2 ⊢ ( I ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} | |
2 | df-mpt 5232 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} | |
3 | 1, 2 | eqtr4i 2762 | 1 ⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1540 ∈ wcel 2105 {copab 5210 ↦ cmpt 5231 I cid 5573 ↾ cres 5678 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-res 5688 |
This theorem is referenced by: idref 7146 2fvcoidd 7298 pwfseqlem5 10664 restid2 17383 curf2ndf 18207 hofcl 18219 yonedainv 18241 smndex2dlinvh 18837 sylow1lem2 19512 sylow3lem1 19540 0frgp 19692 frgpcyg 21352 evpmodpmf1o 21372 cnmptid 23398 txswaphmeolem 23541 idnghm 24493 dvexp 25718 dvmptid 25722 mvth 25758 plyid 25972 coeidp 26027 dgrid 26028 plyremlem 26067 taylply2 26130 wilthlem2 26824 ftalem7 26834 fusgrfis 28869 fzto1st1 32546 cycpm2tr 32563 zrhre 33312 qqhre 33313 fsovcnvlem 43079 fourierdlem60 45193 fourierdlem61 45194 itcoval0mpt 47452 |
Copyright terms: Public domain | W3C validator |