Theorem mptresid 6055

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

Syntax hints:   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {copab 5174   ↦ cmpt 5193   I cid 5557   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-res 5675

This theorem is referenced by:  idref  7144  2fvcoidd  7297  pwfseqlem5  10649  restid2  17484  curf2ndf  18304  hofcl  18316  yonedainv  18338  smndex2dlinvh  18980  sylow1lem2  19670  sylow3lem1  19698  0frgp  19850  frgpcyg  21704  evpmodpmf1o  21727  cnmptid  23799  txswaphmeolem  23942  idnghm  24881  dvexp  26093  dvmptid  26097  mvth  26132  plyid  26347  coeidp  26401  dgrid  26402  plyremlem  26446  taylply2  26509  wilthlem2  27211  ftalem7  27221  fusgrfis  29658  fzto1st1  33400  cycpm2tr  33417  zrhre  34387  qqhre  34388  fsovcnvlem  44719  fourierdlem60  46860  fourierdlem61  46861  itcoval0mpt  49423