Theorem f1oi 6801

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 6610	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		cnvresid 6560	. . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
3	2	fneq1i 6578	. . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
4	1, 3	mpbir 231	. 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴
5		dff1o4 6771	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴))
6	1, 4, 5	mpbir2an 711	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   I cid 5510  ^◡ccnv 5615   ↾ cres 5618   Fn wfn 6476  –1-1-onto→wf1o 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-opab 5154  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488

This theorem is referenced by:  f1ovi  6802  fveqf1o  7236  f1ofvswap  7240  isoid  7263  enrefg  8906  ssdomg  8922  enreffi  9092  ssdomfi  9105  ssdomfi2  9106  wdomref  9458  infxpenc  9909  pwfseqlem5  10554  fproddvdsd  16246  wunndx  17106  idfucl  17788  idffth  17842  ressffth  17847  setccatid  17991  estrccatid  18038  funcestrcsetclem7  18052  funcestrcsetclem8  18053  equivestrcsetc  18058  funcsetcestrclem7  18067  funcsetcestrclem8  18068  idmgmhm  18609  idmhm  18703  ielefmnd  18795  sursubmefmnd  18804  injsubmefmnd  18805  idghm  19144  idresperm  19299  islinds2  21751  lindfres  21761  lindsmm  21766  mdetunilem9  22536  ssidcn  23171  resthauslem  23279  sshauslem  23288  idqtop  23622  fmid  23876  iducn  24198  mbfid  25564  dvid  25847  dvexp  25885  wilthlem2  27007  wilthlem3  27008  idmot  28516  ausgrusgrb  29144  upgrres1  29292  umgrres1  29293  usgrres1  29294  usgrexilem  29419  sizusglecusglem1  29441  pliguhgr  30464  hoif  31732  idunop  31956  idcnop  31959  elunop2  31991  fcobijfs  32702  fcobijfs2  32703  symgcom  33050  fzo0pmtrlast  33059  pmtridf1o  33061  cycpmfvlem  33079  cycpmfv3  33082  cycpmcl  33083  islinds5  33330  ellspds  33331  qqhre  34031  rrhre  34032  subfacp1lem4  35225  subfacp1lem5  35226  poimirlem15  37681  poimirlem22  37688  idlaut  40141  tendoidcl  40814  tendo0co2  40833  erng1r  41040  dvalveclem  41070  dva0g  41072  dvh0g  41156  mzpresrename  42789  eldioph2lem1  42799  eldioph2lem2  42800  diophren  42852  kelac2  43104  lnrfg  43158  fundcmpsurbijinjpreimafv  47444  fundcmpsurinjimaid  47448  grimidvtxedg  47922  ushggricedg  47964  stgrusgra  47996  grlicref  48049  gpgusgra  48094  gpg5grlim  48130  uspgrsprfo  48185  funcringcsetcALTV2lem8  48334  funcringcsetclem8ALTV  48357  itcovalendof  48707  tposidf1o  48924  idfu1stf1o  49137  imaidfu  49148  idfth  49196  idsubc  49198  fucoppc  49448  oduoppcciso  49604