Theorem mptresid 5920

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

Syntax hints:   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {copab 5130   ↦ cmpt 5148   I cid 5461   ↾ cres 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-res 5569

This theorem is referenced by:  idref  6910  2fvcoidd  7055  pwfseqlem5  10087  restid2  16706  curf2ndf  17499  hofcl  17511  yonedainv  17533  smndex2dlinvh  18084  sylow1lem2  18726  sylow3lem1  18754  0frgp  18907  frgpcyg  20722  evpmodpmf1o  20742  cnmptid  22271  txswaphmeolem  22414  idnghm  23354  dvexp  24552  dvmptid  24556  mvth  24591  plyid  24801  coeidp  24855  dgrid  24856  plyremlem  24895  taylply2  24958  wilthlem2  25648  ftalem7  25658  fusgrfis  27114  fzto1st1  30746  cycpm2tr  30763  zrhre  31262  qqhre  31263  fsovcnvlem  40366  fourierdlem60  42458  fourierdlem61  42459