Theorem f1oi 6841

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

Syntax hints:   I cid 5535  ^◡ccnv 5640   ↾ cres 5643   Fn wfn 6509  –1-1-onto→wf1o 6513

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521

This theorem is referenced by:  f1ovi  6842  fveqf1o  7280  f1ofvswap  7284  isoid  7307  enrefg  8958  ssdomg  8974  enreffi  9153  ssdomfi  9166  ssdomfi2  9167  wdomref  9532  infxpenc  9978  pwfseqlem5  10623  fproddvdsd  16312  wunndx  17172  idfucl  17850  idffth  17904  ressffth  17909  setccatid  18053  estrccatid  18100  funcestrcsetclem7  18114  funcestrcsetclem8  18115  equivestrcsetc  18120  funcsetcestrclem7  18129  funcsetcestrclem8  18130  idmgmhm  18635  idmhm  18729  ielefmnd  18821  sursubmefmnd  18830  injsubmefmnd  18831  idghm  19170  idresperm  19323  islinds2  21729  lindfres  21739  lindsmm  21744  mdetunilem9  22514  ssidcn  23149  resthauslem  23257  sshauslem  23266  idqtop  23600  fmid  23854  iducn  24177  mbfid  25543  dvid  25826  dvexp  25864  wilthlem2  26986  wilthlem3  26987  idmot  28471  ausgrusgrb  29099  upgrres1  29247  umgrres1  29248  usgrres1  29249  usgrexilem  29374  sizusglecusglem1  29396  pliguhgr  30422  hoif  31690  idunop  31914  idcnop  31917  elunop2  31949  fcobijfs  32653  symgcom  33047  fzo0pmtrlast  33056  pmtridf1o  33058  cycpmfvlem  33076  cycpmfv3  33079  cycpmcl  33080  islinds5  33345  ellspds  33346  qqhre  34017  rrhre  34018  subfacp1lem4  35177  subfacp1lem5  35178  poimirlem15  37636  poimirlem22  37643  idlaut  40097  tendoidcl  40770  tendo0co2  40789  erng1r  40996  dvalveclem  41026  dva0g  41028  dvh0g  41112  mzpresrename  42745  eldioph2lem1  42755  eldioph2lem2  42756  diophren  42808  kelac2  43061  lnrfg  43115  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  grimidvtxedg  47889  ushggricedg  47931  stgrusgra  47962  grlicref  48008  gpgusgra  48052  uspgrsprfo  48140  funcringcsetcALTV2lem8  48289  funcringcsetclem8ALTV  48312  itcovalendof  48662  tposidf1o  48879  idfu1stf1o  49092  imaidfu  49103  idfth  49151  idsubc  49153  fucoppc  49403  oduoppcciso  49559