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 6646	. . . 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 5581  ^◡ccnv 5687   ↾ cres 5690   Fn wfn 6557  –1-1-onto→wf1o 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569

This theorem is referenced by:  f1ovi  6887  fveqf1o  7321  f1ofvswap  7325  isoid  7348  enrefg  9022  ssdomg  9038  enreffi  9220  ssdomfi  9233  ssdomfi2  9234  wdomref  9609  infxpenc  10055  pwfseqlem5  10700  fproddvdsd  16368  wunndx  17228  idfucl  17931  idffth  17986  ressffth  17991  setccatid  18137  estrccatid  18186  funcestrcsetclem7  18201  funcestrcsetclem8  18202  equivestrcsetc  18207  funcsetcestrclem7  18216  funcsetcestrclem8  18217  idmgmhm  18726  idmhm  18820  ielefmnd  18912  sursubmefmnd  18921  injsubmefmnd  18922  idghm  19261  idresperm  19417  islinds2  21850  lindfres  21860  lindsmm  21865  mdetunilem9  22641  ssidcn  23278  resthauslem  23386  sshauslem  23395  idqtop  23729  fmid  23983  iducn  24307  mbfid  25683  dvid  25967  dvexp  26005  wilthlem2  27126  wilthlem3  27127  idmot  28559  ausgrusgrb  29196  upgrres1  29344  umgrres1  29345  usgrres1  29346  usgrexilem  29471  sizusglecusglem1  29493  pliguhgr  30514  hoif  31782  idunop  32006  idcnop  32009  elunop2  32041  fcobijfs  32740  symgcom  33085  fzo0pmtrlast  33094  pmtridf1o  33096  cycpmfvlem  33114  cycpmfv3  33117  cycpmcl  33118  islinds5  33374  ellspds  33375  qqhre  33982  rrhre  33983  subfacp1lem4  35167  subfacp1lem5  35168  poimirlem15  37621  poimirlem22  37628  idlaut  40078  tendoidcl  40751  tendo0co2  40770  erng1r  40977  dvalveclem  41007  dva0g  41009  dvh0g  41093  mzpresrename  42737  eldioph2lem1  42747  eldioph2lem2  42748  diophren  42800  kelac2  43053  lnrfg  43107  fundcmpsurbijinjpreimafv  47331  fundcmpsurinjimaid  47335  grimidvtxedg  47813  ushggricedg  47833  stgrusgra  47861  grlicref  47907  gpgusgra  47946  uspgrsprfo  47991  funcringcsetcALTV2lem8  48140  funcringcsetclem8ALTV  48163  itcovalendof  48518  oduoppcciso  48881