Theorem f1oi 6737

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 6545	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		cnvresid 6497	. . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
3	2	fneq1i 6514	. . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
4	1, 3	mpbir 230	. 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴
5		dff1o4 6708	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴))
6	1, 4, 5	mpbir2an 707	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   I cid 5479  ^◡ccnv 5579   ↾ cres 5582   Fn wfn 6413  –1-1-onto→wf1o 6417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425

This theorem is referenced by:  f1ovi  6738  fveqf1o  7155  f1ofvswap  7158  isoid  7180  enrefg  8727  ssdomg  8741  enreffi  8929  ssdomfi  8940  wdomref  9261  infxpenc  9705  pwfseqlem5  10350  fproddvdsd  15972  wunndx  16824  idfucl  17512  idffth  17565  ressffth  17570  setccatid  17715  estrccatid  17764  funcestrcsetclem7  17779  funcestrcsetclem8  17780  equivestrcsetc  17785  funcsetcestrclem7  17794  funcsetcestrclem8  17795  idmhm  18354  ielefmnd  18441  sursubmefmnd  18450  injsubmefmnd  18451  idghm  18764  idresperm  18908  islinds2  20930  lindfres  20940  lindsmm  20945  mdetunilem9  21677  ssidcn  22314  resthauslem  22422  sshauslem  22431  idqtop  22765  fmid  23019  iducn  23343  mbfid  24704  dvid  24987  dvexp  25022  wilthlem2  26123  wilthlem3  26124  idmot  26802  ausgrusgrb  27438  upgrres1  27583  umgrres1  27584  usgrres1  27585  usgrexilem  27710  sizusglecusglem1  27731  pliguhgr  28749  hoif  30017  idunop  30241  idcnop  30244  elunop2  30276  fcobijfs  30960  symgcom  31254  pmtridf1o  31263  cycpmfvlem  31281  cycpmfv3  31284  cycpmcl  31285  islinds5  31465  ellspds  31466  qqhre  31870  rrhre  31871  subfacp1lem4  33045  subfacp1lem5  33046  poimirlem15  35719  poimirlem22  35726  idlaut  38037  tendoidcl  38710  tendo0co2  38729  erng1r  38936  dvalveclem  38966  dva0g  38968  dvh0g  39052  mzpresrename  40488  eldioph2lem1  40498  eldioph2lem2  40499  diophren  40551  kelac2  40806  lnrfg  40860  fundcmpsurbijinjpreimafv  44747  fundcmpsurinjimaid  44751  isomgreqve  45165  ushrisomgr  45181  uspgrsprfo  45198  idmgmhm  45230  funcringcsetcALTV2lem8  45489  funcringcsetclem8ALTV  45512  itcovalendof  45903