Theorem mptresid 6048

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

Syntax hints:   ∧ wa 395   = wceq 1534   ∈ wcel 2099  {copab 5204   ↦ cmpt 5225   I cid 5569   ↾ cres 5674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-res 5684

This theorem is referenced by:  idref  7149  2fvcoidd  7300  pwfseqlem5  10678  restid2  17403  curf2ndf  18230  hofcl  18242  yonedainv  18264  smndex2dlinvh  18860  sylow1lem2  19545  sylow3lem1  19573  0frgp  19725  frgpcyg  21494  evpmodpmf1o  21515  cnmptid  23552  txswaphmeolem  23695  idnghm  24647  dvexp  25872  dvmptid  25876  mvth  25912  plyid  26130  coeidp  26185  dgrid  26186  plyremlem  26226  taylply2  26289  taylply2OLD  26290  wilthlem2  26988  ftalem7  26998  fusgrfis  29130  fzto1st1  32801  cycpm2tr  32818  zrhre  33556  qqhre  33557  fsovcnvlem  43366  fourierdlem60  45477  fourierdlem61  45478  itcoval0mpt  47662