Theorem f1oi 6756

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 6563	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		cnvresid 6515	. . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
3	2	fneq1i 6532	. . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
4	1, 3	mpbir 230	. 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴
5		dff1o4 6726	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴))
6	1, 4, 5	mpbir2an 708	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   I cid 5490  ^◡ccnv 5590   ↾ cres 5593   Fn wfn 6430  –1-1-onto→wf1o 6434

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5225  ax-nul 5232  ax-pr 5354

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3433  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-sn 4564  df-pr 4566  df-op 4570  df-br 5077  df-opab 5139  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-fun 6437  df-fn 6438  df-f 6439  df-f1 6440  df-fo 6441  df-f1o 6442

This theorem is referenced by:  f1ovi  6757  fveqf1o  7177  f1ofvswap  7180  isoid  7202  enrefg  8770  ssdomg  8784  enreffi  8967  ssdomfi  8980  ssdomfi2  8981  wdomref  9329  infxpenc  9772  pwfseqlem5  10417  fproddvdsd  16042  wunndx  16894  idfucl  17594  idffth  17647  ressffth  17652  setccatid  17797  estrccatid  17846  funcestrcsetclem7  17861  funcestrcsetclem8  17862  equivestrcsetc  17867  funcsetcestrclem7  17876  funcsetcestrclem8  17877  idmhm  18437  ielefmnd  18524  sursubmefmnd  18533  injsubmefmnd  18534  idghm  18847  idresperm  18991  islinds2  21018  lindfres  21028  lindsmm  21033  mdetunilem9  21767  ssidcn  22404  resthauslem  22512  sshauslem  22521  idqtop  22855  fmid  23109  iducn  23433  mbfid  24797  dvid  25080  dvexp  25115  wilthlem2  26216  wilthlem3  26217  idmot  26896  ausgrusgrb  27533  upgrres1  27678  umgrres1  27679  usgrres1  27680  usgrexilem  27805  sizusglecusglem1  27826  pliguhgr  28845  hoif  30113  idunop  30337  idcnop  30340  elunop2  30372  fcobijfs  31055  symgcom  31349  pmtridf1o  31358  cycpmfvlem  31376  cycpmfv3  31379  cycpmcl  31380  islinds5  31560  ellspds  31561  qqhre  31967  rrhre  31968  subfacp1lem4  33142  subfacp1lem5  33143  poimirlem15  35789  poimirlem22  35796  idlaut  38107  tendoidcl  38780  tendo0co2  38799  erng1r  39006  dvalveclem  39036  dva0g  39038  dvh0g  39122  mzpresrename  40569  eldioph2lem1  40579  eldioph2lem2  40580  diophren  40632  kelac2  40887  lnrfg  40941  fundcmpsurbijinjpreimafv  44826  fundcmpsurinjimaid  44830  isomgreqve  45244  ushrisomgr  45260  uspgrsprfo  45277  idmgmhm  45309  funcringcsetcALTV2lem8  45568  funcringcsetclem8ALTV  45591  itcovalendof  45982