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 5891 | . 2 ⊢ ( I ↾ 𝐴) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} | |
2 | df-mpt 5111 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)} | |
3 | 1, 2 | eqtr4i 2764 | 1 ⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 399 = wceq 1542 ∈ wcel 2114 {copab 5092 ↦ cmpt 5110 I cid 5428 ↾ cres 5527 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-12 2179 ax-ext 2710 ax-sep 5167 ax-nul 5174 ax-pr 5296 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-rab 3062 df-v 3400 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-nul 4212 df-if 4415 df-sn 4517 df-pr 4519 df-op 4523 df-opab 5093 df-mpt 5111 df-id 5429 df-xp 5531 df-rel 5532 df-res 5537 |
This theorem is referenced by: idref 6918 2fvcoidd 7064 pwfseqlem5 10163 restid2 16807 curf2ndf 17613 hofcl 17625 yonedainv 17647 smndex2dlinvh 18198 sylow1lem2 18842 sylow3lem1 18870 0frgp 19023 frgpcyg 20392 evpmodpmf1o 20412 cnmptid 22412 txswaphmeolem 22555 idnghm 23496 dvexp 24705 dvmptid 24709 mvth 24744 plyid 24958 coeidp 25012 dgrid 25013 plyremlem 25052 taylply2 25115 wilthlem2 25806 ftalem7 25816 fusgrfis 27272 fzto1st1 30946 cycpm2tr 30963 zrhre 31539 qqhre 31540 fsovcnvlem 41167 fourierdlem60 43249 fourierdlem61 43250 itcoval0mpt 45546 |
Copyright terms: Public domain | W3C validator |