Theorem mptresid 6050

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

Syntax hints:   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {copab 5210   ↦ cmpt 5231   I cid 5573   ↾ cres 5678

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-res 5688

This theorem is referenced by:  idref  7146  2fvcoidd  7297  pwfseqlem5  10660  restid2  17378  curf2ndf  18202  hofcl  18214  yonedainv  18236  smndex2dlinvh  18800  sylow1lem2  19469  sylow3lem1  19497  0frgp  19649  frgpcyg  21135  evpmodpmf1o  21155  cnmptid  23172  txswaphmeolem  23315  idnghm  24267  dvexp  25477  dvmptid  25481  mvth  25516  plyid  25730  coeidp  25784  dgrid  25785  plyremlem  25824  taylply2  25887  wilthlem2  26580  ftalem7  26590  fusgrfis  28625  fzto1st1  32302  cycpm2tr  32319  zrhre  33068  qqhre  33069  fsovcnvlem  42846  fourierdlem60  44961  fourierdlem61  44962  itcoval0mpt  47430