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

Theorem fnresi 5654
Description: Functionality and domain of restricted identity. (Contributed by NM, 27-Aug-2004.)
Assertion
Ref Expression
fnresi  |-  (  _I  |`  A )  Fn  A

Proof of Theorem fnresi
StepHypRef Expression
1 funi 5574 . . 3  |-  Fun  _I
2 funres 5583 . . 3  |-  ( Fun 
_I  ->  Fun  (  _I  |`  A ) )
31, 2ax-mp 5 . 2  |-  Fun  (  _I  |`  A )
4 dmresi 5122 . 2  |-  dom  (  _I  |`  A )  =  A
5 df-fn 5547 . 2  |-  ( (  _I  |`  A )  Fn  A  <->  ( Fun  (  _I  |`  A )  /\  dom  (  _I  |`  A )  =  A ) )
63, 4, 5mpbir2an 928 1  |-  (  _I  |`  A )  Fn  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    _I cid 4706   dom cdm 4796    |` cres 4798   Fun wfun 5538    Fn wfn 5539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-res 4808  df-fun 5546  df-fn 5547
This theorem is referenced by:  f1oi  5810  fninfp  6050  fndifnfp  6052  fnnfpeq0  6054  fveqf1o  6159  weniso  6204  iordsmo  7031  fipreima  7833  dfac9  8517  pmtrfinv  17045  ustuqtop3  21200  fta1blem  23061  qaa  23221  dfiop2  27348  idssxp  28173  cvmliftlem4  29963  cvmliftlem5  29964  poimirlem15  31862  poimirlem22  31869  ltrnid  33612  rtrclex  36137  dvsid  36593  dflinc2  39796
  Copyright terms: Public domain W3C validator