Theorem mptresid 6018

Description: The restricted identity relation expressed in maps-to notation. (Contributed by FL, 25-Apr-2012.)

Assertion

Ref	Expression
mptresid	⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)

Distinct variable group:   𝑥,𝐴

Proof of Theorem mptresid

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opabresid 6017	. 2 ⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
2		df-mpt 5182	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
3	1, 2	eqtr4i 2763	1 ⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)

Syntax hints:   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5162   ↦ cmpt 5181   I cid 5526   ↾ cres 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-res 5644

This theorem is referenced by:  idref  7101  2fvcoidd  7253  pwfseqlem5  10586  restid2  17362  curf2ndf  18182  hofcl  18194  yonedainv  18216  smndex2dlinvh  18854  sylow1lem2  19540  sylow3lem1  19568  0frgp  19720  frgpcyg  21540  evpmodpmf1o  21563  cnmptid  23617  txswaphmeolem  23760  idnghm  24699  dvexp  25925  dvmptid  25929  mvth  25965  plyid  26182  coeidp  26237  dgrid  26238  plyremlem  26280  taylply2  26343  taylply2OLD  26344  wilthlem2  27047  ftalem7  27057  fusgrfis  29415  fzto1st1  33195  cycpm2tr  33212  zrhre  34196  qqhre  34197  fsovcnvlem  44363  fourierdlem60  46518  fourierdlem61  46519  itcoval0mpt  49020