MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mptresid Structured version   Unicode version

Theorem mptresid 5319
Description: The restricted identity expressed with the "maps to" notation. (Contributed by FL, 25-Apr-2012.)
Assertion
Ref Expression
mptresid  |-  ( x  e.  A  |->  x )  =  (  _I  |`  A )
Distinct variable group:    x, A

Proof of Theorem mptresid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-mpt 4500 . 2  |-  ( x  e.  A  |->  x )  =  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  x ) }
2 opabresid 5318 . 2  |-  { <. x ,  y >.  |  ( x  e.  A  /\  y  =  x ) }  =  (  _I  |`  A )
31, 2eqtri 2489 1  |-  ( x  e.  A  |->  x )  =  (  _I  |`  A )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1374    e. wcel 1762   {copab 4497    |-> cmpt 4498    _I cid 4783    |` cres 4994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-res 5004
This theorem is referenced by:  idref  6132  2fvcoidd  6179  pwfseqlem5  9030  restid2  14675  curf2ndf  15363  hofcl  15375  yonedainv  15397  sylow1lem2  16408  sylow3lem1  16436  0frgp  16586  frgpcyg  18372  evpmodpmf1o  18392  txswaphmeolem  20033  idnghm  20978  dvexp  22084  dvmptid  22088  mvth  22121  plyid  22334  coeidp  22387  dgrid  22388  plyremlem  22427  taylply2  22490  wilthlem2  23064  ftalem7  23073  zrhre  27619  qqhre  27620  fourierdlem60  31422  fourierdlem61  31423  usgfis  31840
  Copyright terms: Public domain W3C validator