Theorem mptresid 6051

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5171   ↦ cmpt 5190   I cid 5553   ↾ cres 5661

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 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-res 5671

This theorem is used by:  idref  7146  2fvcoidd  7302  pwfseqlem5  10676  restid2  17521  curf2ndf  18341  hofcl  18353  yonedainv  18375  smndex2dlinvh  19035  sylow1lem2  19732  sylow3lem1  19760  0frgp  19912  frgpcyg  21792  evpmodpmf1o  21815  cnmptid  23893  txswaphmeolem  24036  idnghm  24975  dvexp  26187  dvmptid  26191  mvth  26226  plyid  26441  coeidp  26496  dgrid  26497  plyremlem  26541  taylply2  26611  wilthlem2  27313  ftalem7  27323  fusgrfis  29798  fzto1st1  33550  cycpm2tr  33567  zrhre  34537  qqhre  34538  fsovcnvlem  44861  fourierdlem60  47002  fourierdlem61  47003  itcoval0mpt  49604