Theorem f1oi 6806

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

Syntax hints:   I cid 5517  ^◡ccnv 5622   ↾ cres 5625   Fn wfn 6481  –1-1-onto→wf1o 6485

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  f1ovi  6807  fveqf1o  7243  f1ofvswap  7247  isoid  7270  enrefg  8916  ssdomg  8932  enreffi  9107  ssdomfi  9120  ssdomfi2  9121  wdomref  9483  infxpenc  9931  pwfseqlem5  10576  fproddvdsd  16264  wunndx  17124  idfucl  17806  idffth  17860  ressffth  17865  setccatid  18009  estrccatid  18056  funcestrcsetclem7  18070  funcestrcsetclem8  18071  equivestrcsetc  18076  funcsetcestrclem7  18085  funcsetcestrclem8  18086  idmgmhm  18593  idmhm  18687  ielefmnd  18779  sursubmefmnd  18788  injsubmefmnd  18789  idghm  19128  idresperm  19283  islinds2  21738  lindfres  21748  lindsmm  21753  mdetunilem9  22523  ssidcn  23158  resthauslem  23266  sshauslem  23275  idqtop  23609  fmid  23863  iducn  24186  mbfid  25552  dvid  25835  dvexp  25873  wilthlem2  26995  wilthlem3  26996  idmot  28500  ausgrusgrb  29128  upgrres1  29276  umgrres1  29277  usgrres1  29278  usgrexilem  29403  sizusglecusglem1  29425  pliguhgr  30448  hoif  31716  idunop  31940  idcnop  31943  elunop2  31975  fcobijfs  32679  symgcom  33038  fzo0pmtrlast  33047  pmtridf1o  33049  cycpmfvlem  33067  cycpmfv3  33070  cycpmcl  33071  islinds5  33317  ellspds  33318  qqhre  33989  rrhre  33990  subfacp1lem4  35158  subfacp1lem5  35159  poimirlem15  37617  poimirlem22  37624  idlaut  40078  tendoidcl  40751  tendo0co2  40770  erng1r  40977  dvalveclem  41007  dva0g  41009  dvh0g  41093  mzpresrename  42726  eldioph2lem1  42736  eldioph2lem2  42737  diophren  42789  kelac2  43041  lnrfg  43095  fundcmpsurbijinjpreimafv  47395  fundcmpsurinjimaid  47399  grimidvtxedg  47873  ushggricedg  47915  stgrusgra  47947  grlicref  48000  gpgusgra  48045  gpg5grlim  48081  uspgrsprfo  48136  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  itcovalendof  48658  tposidf1o  48875  idfu1stf1o  49088  imaidfu  49099  idfth  49147  idsubc  49149  fucoppc  49399  oduoppcciso  49555