Theorem mptresid 6045

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5167   ↦ cmpt 5186   I cid 5545   ↾ cres 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-res 5663

This theorem is used by:  idref  7141  2fvcoidd  7297  pwfseqlem5  10729  restid2  17581  curf2ndf  18401  hofcl  18413  yonedainv  18435  smndex2dlinvh  19096  sylow1lem2  19793  sylow3lem1  19821  0frgp  19973  frgpcyg  21859  evpmodpmf1o  21882  cnmptid  23960  txswaphmeolem  24103  idnghm  25042  dvexp  26253  dvmptid  26257  mvth  26292  plyid  26507  coeidp  26562  dgrid  26563  plyremlem  26607  taylply2  26677  wilthlem2  27378  ftalem7  27388  fusgrfis  29893  fzto1st1  33645  cycpm2tr  33662  zrhre  34633  qqhre  34634  fsovcnvlem  44972  fourierdlem60  47120  fourierdlem61  47121  itcoval0mpt  49722