Theorem mptresid 6004

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5155   ↦ cmpt 5174   I cid 5513   ↾ cres 5621

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-res 5631

This theorem is referenced by:  idref  7085  2fvcoidd  7237  pwfseqlem5  10561  restid2  17336  curf2ndf  18155  hofcl  18167  yonedainv  18189  smndex2dlinvh  18827  sylow1lem2  19513  sylow3lem1  19541  0frgp  19693  frgpcyg  21512  evpmodpmf1o  21535  cnmptid  23577  txswaphmeolem  23720  idnghm  24659  dvexp  25885  dvmptid  25889  mvth  25925  plyid  26142  coeidp  26197  dgrid  26198  plyremlem  26240  taylply2  26303  taylply2OLD  26304  wilthlem2  27007  ftalem7  27017  fusgrfis  29310  fzto1st1  33078  cycpm2tr  33095  zrhre  34053  qqhre  34054  fsovcnvlem  44130  fourierdlem60  46288  fourierdlem61  46289  itcoval0mpt  48791