Theorem f1oi 6754

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

Syntax hints:   I cid 5488  ^◡ccnv 5588   ↾ cres 5591   Fn wfn 6428  –1-1-onto→wf1o 6432

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 5223  ax-nul 5230  ax-pr 5352

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 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440

This theorem is referenced by:  f1ovi  6755  fveqf1o  7175  f1ofvswap  7178  isoid  7200  enrefg  8772  ssdomg  8786  enreffi  8969  ssdomfi  8982  ssdomfi2  8983  wdomref  9331  infxpenc  9774  pwfseqlem5  10419  fproddvdsd  16044  wunndx  16896  idfucl  17596  idffth  17649  ressffth  17654  setccatid  17799  estrccatid  17848  funcestrcsetclem7  17863  funcestrcsetclem8  17864  equivestrcsetc  17869  funcsetcestrclem7  17878  funcsetcestrclem8  17879  idmhm  18439  ielefmnd  18526  sursubmefmnd  18535  injsubmefmnd  18536  idghm  18849  idresperm  18993  islinds2  21020  lindfres  21030  lindsmm  21035  mdetunilem9  21769  ssidcn  22406  resthauslem  22514  sshauslem  22523  idqtop  22857  fmid  23111  iducn  23435  mbfid  24799  dvid  25082  dvexp  25117  wilthlem2  26218  wilthlem3  26219  idmot  26898  ausgrusgrb  27535  upgrres1  27680  umgrres1  27681  usgrres1  27682  usgrexilem  27807  sizusglecusglem1  27828  pliguhgr  28848  hoif  30116  idunop  30340  idcnop  30343  elunop2  30375  fcobijfs  31058  symgcom  31352  pmtridf1o  31361  cycpmfvlem  31379  cycpmfv3  31382  cycpmcl  31383  islinds5  31563  ellspds  31564  qqhre  31970  rrhre  31971  subfacp1lem4  33145  subfacp1lem5  33146  poimirlem15  35792  poimirlem22  35799  idlaut  38110  tendoidcl  38783  tendo0co2  38802  erng1r  39009  dvalveclem  39039  dva0g  39041  dvh0g  39125  mzpresrename  40572  eldioph2lem1  40582  eldioph2lem2  40583  diophren  40635  kelac2  40890  lnrfg  40944  fundcmpsurbijinjpreimafv  44859  fundcmpsurinjimaid  44863  isomgreqve  45277  ushrisomgr  45293  uspgrsprfo  45310  idmgmhm  45342  funcringcsetcALTV2lem8  45601  funcringcsetclem8ALTV  45624  itcovalendof  46015