Theorem f1oi 6856

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

Syntax hints:   I cid 5547  ^◡ccnv 5653   ↾ cres 5656   Fn wfn 6526  –1-1-onto→wf1o 6530

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538

This theorem is referenced by:  f1ovi  6857  fveqf1o  7295  f1ofvswap  7299  isoid  7322  enrefg  8998  ssdomg  9014  enreffi  9197  ssdomfi  9210  ssdomfi2  9211  wdomref  9586  infxpenc  10032  pwfseqlem5  10677  fproddvdsd  16354  wunndx  17214  idfucl  17894  idffth  17948  ressffth  17953  setccatid  18097  estrccatid  18144  funcestrcsetclem7  18158  funcestrcsetclem8  18159  equivestrcsetc  18164  funcsetcestrclem7  18173  funcsetcestrclem8  18174  idmgmhm  18679  idmhm  18773  ielefmnd  18865  sursubmefmnd  18874  injsubmefmnd  18875  idghm  19214  idresperm  19367  islinds2  21773  lindfres  21783  lindsmm  21788  mdetunilem9  22558  ssidcn  23193  resthauslem  23301  sshauslem  23310  idqtop  23644  fmid  23898  iducn  24221  mbfid  25588  dvid  25871  dvexp  25909  wilthlem2  27031  wilthlem3  27032  idmot  28516  ausgrusgrb  29144  upgrres1  29292  umgrres1  29293  usgrres1  29294  usgrexilem  29419  sizusglecusglem1  29441  pliguhgr  30467  hoif  31735  idunop  31959  idcnop  31962  elunop2  31994  fcobijfs  32700  symgcom  33094  fzo0pmtrlast  33103  pmtridf1o  33105  cycpmfvlem  33123  cycpmfv3  33126  cycpmcl  33127  islinds5  33382  ellspds  33383  qqhre  34051  rrhre  34052  subfacp1lem4  35205  subfacp1lem5  35206  poimirlem15  37659  poimirlem22  37666  idlaut  40115  tendoidcl  40788  tendo0co2  40807  erng1r  41014  dvalveclem  41044  dva0g  41046  dvh0g  41130  mzpresrename  42773  eldioph2lem1  42783  eldioph2lem2  42784  diophren  42836  kelac2  43089  lnrfg  43143  fundcmpsurbijinjpreimafv  47421  fundcmpsurinjimaid  47425  grimidvtxedg  47898  ushggricedg  47940  stgrusgra  47971  grlicref  48017  gpgusgra  48061  uspgrsprfo  48123  funcringcsetcALTV2lem8  48272  funcringcsetclem8ALTV  48295  itcovalendof  48649  tposidf1o  48862  imaidfu  49069  idfth  49098  idsubc  49099  oduoppcciso  49443