Theorem mptresid 6000

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

Syntax hints:   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {copab 5153   ↦ cmpt 5172   I cid 5510   ↾ cres 5618

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 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-res 5628

This theorem is referenced by:  idref  7079  2fvcoidd  7231  pwfseqlem5  10551  restid2  17331  curf2ndf  18150  hofcl  18162  yonedainv  18184  smndex2dlinvh  18822  sylow1lem2  19509  sylow3lem1  19537  0frgp  19689  frgpcyg  21508  evpmodpmf1o  21531  cnmptid  23574  txswaphmeolem  23717  idnghm  24656  dvexp  25882  dvmptid  25886  mvth  25922  plyid  26139  coeidp  26194  dgrid  26195  plyremlem  26237  taylply2  26300  taylply2OLD  26301  wilthlem2  27004  ftalem7  27014  fusgrfis  29306  fzto1st1  33066  cycpm2tr  33083  zrhre  34027  qqhre  34028  fsovcnvlem  44045  fourierdlem60  46203  fourierdlem61  46204  itcoval0mpt  48697