Theorem f1oi 6838

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

Syntax hints:   I cid 5532  ^◡ccnv 5637   ↾ cres 5640   Fn wfn 6506  –1-1-onto→wf1o 6510

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-id 5533  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 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1ovi  6839  fveqf1o  7277  f1ofvswap  7281  isoid  7304  enrefg  8955  ssdomg  8971  enreffi  9147  ssdomfi  9160  ssdomfi2  9161  wdomref  9525  infxpenc  9971  pwfseqlem5  10616  fproddvdsd  16305  wunndx  17165  idfucl  17843  idffth  17897  ressffth  17902  setccatid  18046  estrccatid  18093  funcestrcsetclem7  18107  funcestrcsetclem8  18108  equivestrcsetc  18113  funcsetcestrclem7  18122  funcsetcestrclem8  18123  idmgmhm  18628  idmhm  18722  ielefmnd  18814  sursubmefmnd  18823  injsubmefmnd  18824  idghm  19163  idresperm  19316  islinds2  21722  lindfres  21732  lindsmm  21737  mdetunilem9  22507  ssidcn  23142  resthauslem  23250  sshauslem  23259  idqtop  23593  fmid  23847  iducn  24170  mbfid  25536  dvid  25819  dvexp  25857  wilthlem2  26979  wilthlem3  26980  idmot  28464  ausgrusgrb  29092  upgrres1  29240  umgrres1  29241  usgrres1  29242  usgrexilem  29367  sizusglecusglem1  29389  pliguhgr  30415  hoif  31683  idunop  31907  idcnop  31910  elunop2  31942  fcobijfs  32646  symgcom  33040  fzo0pmtrlast  33049  pmtridf1o  33051  cycpmfvlem  33069  cycpmfv3  33072  cycpmcl  33073  islinds5  33338  ellspds  33339  qqhre  34010  rrhre  34011  subfacp1lem4  35170  subfacp1lem5  35171  poimirlem15  37629  poimirlem22  37636  idlaut  40090  tendoidcl  40763  tendo0co2  40782  erng1r  40989  dvalveclem  41019  dva0g  41021  dvh0g  41105  mzpresrename  42738  eldioph2lem1  42748  eldioph2lem2  42749  diophren  42801  kelac2  43054  lnrfg  43108  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  grimidvtxedg  47885  ushggricedg  47927  stgrusgra  47958  grlicref  48004  gpgusgra  48048  uspgrsprfo  48136  funcringcsetcALTV2lem8  48285  funcringcsetclem8ALTV  48308  itcovalendof  48658  tposidf1o  48875  idfu1stf1o  49088  imaidfu  49099  idfth  49147  idsubc  49149  fucoppc  49399  oduoppcciso  49555