Theorem f1oi 6886

Description: A restriction of the identity relation is a one-to-one onto function. (Contributed by NM, 30-Apr-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)

Assertion

Ref	Expression
f1oi	⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Proof of Theorem f1oi

Step	Hyp	Ref	Expression
1		fnresi 6697	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		cnvresid 6645	. . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
3	2	fneq1i 6665	. . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
4	1, 3	mpbir 231	. 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴
5		dff1o4 6856	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴))
6	1, 4, 5	mpbir2an 711	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   I cid 5577  ^◡ccnv 5684   ↾ cres 5687   Fn wfn 6556  –1-1-onto→wf1o 6560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568

This theorem is referenced by:  f1ovi  6887  fveqf1o  7322  f1ofvswap  7326  isoid  7349  enrefg  9024  ssdomg  9040  enreffi  9223  ssdomfi  9236  ssdomfi2  9237  wdomref  9612  infxpenc  10058  pwfseqlem5  10703  fproddvdsd  16372  wunndx  17232  idfucl  17926  idffth  17980  ressffth  17985  setccatid  18129  estrccatid  18176  funcestrcsetclem7  18191  funcestrcsetclem8  18192  equivestrcsetc  18197  funcsetcestrclem7  18206  funcsetcestrclem8  18207  idmgmhm  18714  idmhm  18808  ielefmnd  18900  sursubmefmnd  18909  injsubmefmnd  18910  idghm  19249  idresperm  19403  islinds2  21833  lindfres  21843  lindsmm  21848  mdetunilem9  22626  ssidcn  23263  resthauslem  23371  sshauslem  23380  idqtop  23714  fmid  23968  iducn  24292  mbfid  25670  dvid  25953  dvexp  25991  wilthlem2  27112  wilthlem3  27113  idmot  28545  ausgrusgrb  29182  upgrres1  29330  umgrres1  29331  usgrres1  29332  usgrexilem  29457  sizusglecusglem1  29479  pliguhgr  30505  hoif  31773  idunop  31997  idcnop  32000  elunop2  32032  fcobijfs  32734  symgcom  33103  fzo0pmtrlast  33112  pmtridf1o  33114  cycpmfvlem  33132  cycpmfv3  33135  cycpmcl  33136  islinds5  33395  ellspds  33396  qqhre  34021  rrhre  34022  subfacp1lem4  35188  subfacp1lem5  35189  poimirlem15  37642  poimirlem22  37649  idlaut  40098  tendoidcl  40771  tendo0co2  40790  erng1r  40997  dvalveclem  41027  dva0g  41029  dvh0g  41113  mzpresrename  42761  eldioph2lem1  42771  eldioph2lem2  42772  diophren  42824  kelac2  43077  lnrfg  43131  fundcmpsurbijinjpreimafv  47394  fundcmpsurinjimaid  47398  grimidvtxedg  47876  ushggricedg  47896  stgrusgra  47926  grlicref  47972  gpgusgra  48012  uspgrsprfo  48064  funcringcsetcALTV2lem8  48213  funcringcsetclem8ALTV  48236  itcovalendof  48590  tposidf1o  48787  oduoppcciso  49170