Theorem mptresid 6025

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

Syntax hints:   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5172   ↦ cmpt 5191   I cid 5535   ↾ cres 5643

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-res 5653

This theorem is referenced by:  idref  7121  2fvcoidd  7275  pwfseqlem5  10623  restid2  17400  curf2ndf  18215  hofcl  18227  yonedainv  18249  smndex2dlinvh  18851  sylow1lem2  19536  sylow3lem1  19564  0frgp  19716  frgpcyg  21490  evpmodpmf1o  21512  cnmptid  23555  txswaphmeolem  23698  idnghm  24638  dvexp  25864  dvmptid  25868  mvth  25904  plyid  26121  coeidp  26176  dgrid  26177  plyremlem  26219  taylply2  26282  taylply2OLD  26283  wilthlem2  26986  ftalem7  26996  fusgrfis  29264  fzto1st1  33066  cycpm2tr  33083  zrhre  34016  qqhre  34017  fsovcnvlem  44009  fourierdlem60  46171  fourierdlem61  46172  itcoval0mpt  48659