Theorem mptresid 6044

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

Syntax hints:   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {copab 5167   ↦ cmpt 5186   I cid 5546   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-res 5664

This theorem is referenced by:  idref  7132  2fvcoidd  7285  pwfseqlem5  10636  restid2  17473  curf2ndf  18293  hofcl  18305  yonedainv  18327  smndex2dlinvh  18969  sylow1lem2  19660  sylow3lem1  19688  0frgp  19840  frgpcyg  21683  evpmodpmf1o  21706  cnmptid  23779  txswaphmeolem  23922  idnghm  24861  dvexp  26073  dvmptid  26077  mvth  26112  plyid  26327  coeidp  26381  dgrid  26382  plyremlem  26426  taylply2  26489  wilthlem2  27191  ftalem7  27201  fusgrfis  29589  fzto1st1  33335  cycpm2tr  33352  zrhre  34326  qqhre  34327  fsovcnvlem  44601  fourierdlem60  46738  fourierdlem61  46739  itcoval0mpt  49297