Theorem mptresid 5885

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

Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {copab 5092   ↦ cmpt 5110   I cid 5424   ↾ cres 5521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-res 5531

This theorem is referenced by:  idref  6885  2fvcoidd  7031  pwfseqlem5  10074  restid2  16696  curf2ndf  17489  hofcl  17501  yonedainv  17523  smndex2dlinvh  18074  sylow1lem2  18716  sylow3lem1  18744  0frgp  18897  frgpcyg  20265  evpmodpmf1o  20285  cnmptid  22266  txswaphmeolem  22409  idnghm  23349  dvexp  24556  dvmptid  24560  mvth  24595  plyid  24806  coeidp  24860  dgrid  24861  plyremlem  24900  taylply2  24963  wilthlem2  25654  ftalem7  25664  fusgrfis  27120  fzto1st1  30794  cycpm2tr  30811  zrhre  31370  qqhre  31371  fsovcnvlem  40714  fourierdlem60  42808  fourierdlem61  42809  itcoval0mpt  45080