Theorem mptresid 6043

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5186   ↦ cmpt 5206   I cid 5552   ↾ cres 5661

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-res 5671

This theorem is referenced by:  idref  7141  2fvcoidd  7295  pwfseqlem5  10682  restid2  17449  curf2ndf  18264  hofcl  18276  yonedainv  18298  smndex2dlinvh  18900  sylow1lem2  19585  sylow3lem1  19613  0frgp  19765  frgpcyg  21539  evpmodpmf1o  21561  cnmptid  23604  txswaphmeolem  23747  idnghm  24687  dvexp  25914  dvmptid  25918  mvth  25954  plyid  26171  coeidp  26226  dgrid  26227  plyremlem  26269  taylply2  26332  taylply2OLD  26333  wilthlem2  27036  ftalem7  27046  fusgrfis  29314  fzto1st1  33118  cycpm2tr  33135  zrhre  34055  qqhre  34056  fsovcnvlem  44004  fourierdlem60  46162  fourierdlem61  46163  itcoval0mpt  48613