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

Theorem mptresid 5891
 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.
StepHypRef Expression
1 opabresid 5890 . 2 ( I ↾ 𝐴) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝑥)}
2 df-mpt 5120 . 2 (𝑥𝐴𝑥) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝑥)}
31, 2eqtr4i 2847 1 ( I ↾ 𝐴) = (𝑥𝐴𝑥)
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538   ∈ wcel 2115  {copab 5101   ↦ cmpt 5119   I cid 5432   ↾ cres 5530 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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303 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 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-opab 5102  df-mpt 5120  df-id 5433  df-xp 5534  df-rel 5535  df-res 5540 This theorem is referenced by:  idref  6881  2fvcoidd  7027  pwfseqlem5  10062  restid2  16683  curf2ndf  17476  hofcl  17488  yonedainv  17510  smndex2dlinvh  18061  sylow1lem2  18703  sylow3lem1  18731  0frgp  18884  frgpcyg  20696  evpmodpmf1o  20716  cnmptid  22245  txswaphmeolem  22388  idnghm  23328  dvexp  24535  dvmptid  24539  mvth  24574  plyid  24785  coeidp  24839  dgrid  24840  plyremlem  24879  taylply2  24942  wilthlem2  25633  ftalem7  25643  fusgrfis  27099  fzto1st1  30752  cycpm2tr  30769  zrhre  31268  qqhre  31269  fsovcnvlem  40526  fourierdlem60  42631  fourierdlem61  42632  itcoval0mpt  44891
 Copyright terms: Public domain W3C validator