Theorem mptresid 6006

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5157   ↦ cmpt 5176   I cid 5517   ↾ cres 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-res 5635

This theorem is referenced by:  idref  7084  2fvcoidd  7238  pwfseqlem5  10576  restid2  17352  curf2ndf  18171  hofcl  18183  yonedainv  18205  smndex2dlinvh  18809  sylow1lem2  19496  sylow3lem1  19524  0frgp  19676  frgpcyg  21498  evpmodpmf1o  21521  cnmptid  23564  txswaphmeolem  23707  idnghm  24647  dvexp  25873  dvmptid  25877  mvth  25913  plyid  26130  coeidp  26185  dgrid  26186  plyremlem  26228  taylply2  26291  taylply2OLD  26292  wilthlem2  26995  ftalem7  27005  fusgrfis  29293  fzto1st1  33057  cycpm2tr  33074  zrhre  33985  qqhre  33986  fsovcnvlem  43986  fourierdlem60  46148  fourierdlem61  46149  itcoval0mpt  48652