Theorem mptresid 5961

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 5960	. 2 ⊢ ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
2		df-mpt 5159	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝑥) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝑥)}
3	1, 2	eqtr4i 2770	1 ⊢ ( I ↾ 𝐴) = (𝑥 ∈ 𝐴 ↦ 𝑥)

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