Theorem f1oi 6876

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 6685	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		cnvresid 6633	. . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
3	2	fneq1i 6652	. . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
4	1, 3	mpbir 230	. 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴
5		dff1o4 6846	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴))
6	1, 4, 5	mpbir2an 709	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   I cid 5575  ^◡ccnv 5677   ↾ cres 5680   Fn wfn 6544  –1-1-onto→wf1o 6548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556

This theorem is referenced by:  f1ovi  6877  fveqf1o  7311  f1ofvswap  7314  isoid  7336  enrefg  9005  ssdomg  9021  enreffi  9211  ssdomfi  9224  ssdomfi2  9225  wdomref  9597  infxpenc  10043  pwfseqlem5  10688  fproddvdsd  16315  wunndx  17167  idfucl  17870  idffth  17925  ressffth  17930  setccatid  18076  estrccatid  18125  funcestrcsetclem7  18140  funcestrcsetclem8  18141  equivestrcsetc  18146  funcsetcestrclem7  18155  funcsetcestrclem8  18156  idmgmhm  18664  idmhm  18755  ielefmnd  18847  sursubmefmnd  18856  injsubmefmnd  18857  idghm  19194  idresperm  19352  islinds2  21764  lindfres  21774  lindsmm  21779  mdetunilem9  22566  ssidcn  23203  resthauslem  23311  sshauslem  23320  idqtop  23654  fmid  23908  iducn  24232  mbfid  25608  dvid  25891  dvexp  25929  wilthlem2  27046  wilthlem3  27047  idmot  28413  ausgrusgrb  29050  upgrres1  29198  umgrres1  29199  usgrres1  29200  usgrexilem  29325  sizusglecusglem1  29347  pliguhgr  30368  hoif  31636  idunop  31860  idcnop  31863  elunop2  31895  fcobijfs  32587  symgcom  32896  fzo0pmtrlast  32905  pmtridf1o  32907  cycpmfvlem  32925  cycpmfv3  32928  cycpmcl  32929  islinds5  33178  ellspds  33179  qqhre  33752  rrhre  33753  subfacp1lem4  34924  subfacp1lem5  34925  poimirlem15  37239  poimirlem22  37246  idlaut  39699  tendoidcl  40372  tendo0co2  40391  erng1r  40598  dvalveclem  40628  dva0g  40630  dvh0g  40714  mzpresrename  42312  eldioph2lem1  42322  eldioph2lem2  42323  diophren  42375  kelac2  42631  lnrfg  42685  fundcmpsurbijinjpreimafv  46884  fundcmpsurinjimaid  46888  grimidvtxedg  47360  ushggricedg  47379  uspgrsprfo  47396  funcringcsetcALTV2lem8  47545  funcringcsetclem8ALTV  47568  itcovalendof  47928