Theorem f1oi 6827

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

Syntax hints:   I cid 5535  ^◡ccnv 5637   ↾ cres 5640   Fn wfn 6496  –1-1-onto→wf1o 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508

This theorem is referenced by:  f1ovi  6828  fveqf1o  7254  f1ofvswap  7257  isoid  7279  enrefg  8931  ssdomg  8947  enreffi  9137  ssdomfi  9150  ssdomfi2  9151  wdomref  9517  infxpenc  9963  pwfseqlem5  10608  fproddvdsd  16228  wunndx  17078  idfucl  17781  idffth  17834  ressffth  17839  setccatid  17984  estrccatid  18033  funcestrcsetclem7  18048  funcestrcsetclem8  18049  equivestrcsetc  18054  funcsetcestrclem7  18063  funcsetcestrclem8  18064  idmhm  18625  ielefmnd  18711  sursubmefmnd  18720  injsubmefmnd  18721  idghm  19037  idresperm  19181  islinds2  21256  lindfres  21266  lindsmm  21271  mdetunilem9  22006  ssidcn  22643  resthauslem  22751  sshauslem  22760  idqtop  23094  fmid  23348  iducn  23672  mbfid  25036  dvid  25319  dvexp  25354  wilthlem2  26455  wilthlem3  26456  idmot  27542  ausgrusgrb  28179  upgrres1  28324  umgrres1  28325  usgrres1  28326  usgrexilem  28451  sizusglecusglem1  28472  pliguhgr  29491  hoif  30759  idunop  30983  idcnop  30986  elunop2  31018  fcobijfs  31708  symgcom  32004  pmtridf1o  32013  cycpmfvlem  32031  cycpmfv3  32034  cycpmcl  32035  islinds5  32228  ellspds  32229  qqhre  32690  rrhre  32691  subfacp1lem4  33864  subfacp1lem5  33865  poimirlem15  36166  poimirlem22  36173  idlaut  38632  tendoidcl  39305  tendo0co2  39324  erng1r  39531  dvalveclem  39561  dva0g  39563  dvh0g  39647  mzpresrename  41131  eldioph2lem1  41141  eldioph2lem2  41142  diophren  41194  kelac2  41450  lnrfg  41504  fundcmpsurbijinjpreimafv  45719  fundcmpsurinjimaid  45723  isomgreqve  46137  ushrisomgr  46153  uspgrsprfo  46170  idmgmhm  46202  funcringcsetcALTV2lem8  46461  funcringcsetclem8ALTV  46484  itcovalendof  46875