Theorem mptresid 6042

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

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {copab 5166   ↦ cmpt 5185   I cid 5544   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-res 5662

This theorem is used by:  idref  7149  2fvcoidd  7305  pwfseqlem5  10751  restid2  17606  curf2ndf  18426  hofcl  18438  yonedainv  18460  smndex2dlinvh  19121  sylow1lem2  19818  sylow3lem1  19846  0frgp  19998  frgpcyg  21884  evpmodpmf1o  21907  cnmptid  23985  txswaphmeolem  24128  idnghm  25067  dvexp  26278  dvmptid  26282  mvth  26317  plyid  26532  coeidp  26587  dgrid  26588  plyremlem  26630  taylply2  26700  wilthlem2  27401  ftalem7  27411  fusgrfis  29916  fzto1st1  33709  cycpm2tr  33726  zrhre  34697  qqhre  34698  fsovcnvlem  45106  fourierdlem60  47269  fourierdlem61  47270  itcoval0mpt  49871  termcpostfix  50765  fuconuniqlem  50874  fuconuniqvalslem  50876