Theorem f1oi 6174

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 6008	. 2 ⊢ ( I ↾ 𝐴) Fn 𝐴
2		cnvresid 5968	. . . 4 ⊢ ◡( I ↾ 𝐴) = ( I ↾ 𝐴)
3	2	fneq1i 5985	. . 3 ⊢ (◡( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
4	1, 3	mpbir 221	. 2 ⊢ ◡( I ↾ 𝐴) Fn 𝐴
5		dff1o4 6145	. 2 ⊢ (( I ↾ 𝐴):𝐴–1-1-onto→𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴 ∧ ◡( I ↾ 𝐴) Fn 𝐴))
6	1, 4, 5	mpbir2an 955	1 ⊢ ( I ↾ 𝐴):𝐴–1-1-onto→𝐴

Syntax hints:   I cid 5023  ^◡ccnv 5113   ↾ cres 5116   Fn wfn 5883  –1-1-onto→wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1ovi  6175  fveqf1o  6557  isoid  6579  enrefg  7987  ssdomg  8001  hartogslem1  8447  wdomref  8477  infxpenc  8841  pwfseqlem5  9485  dfle2  11980  fproddvdsd  15059  wunndx  15878  idfucl  16541  idffth  16593  ressffth  16598  setccatid  16734  estrccatid  16772  funcestrcsetclem7  16786  funcestrcsetclem8  16787  equivestrcsetc  16792  funcsetcestrclem7  16801  funcsetcestrclem8  16802  idmhm  17344  idghm  17675  symggrp  17820  symgid  17821  idresperm  17829  islinds2  20152  lindfres  20162  lindsmm  20167  mdetunilem9  20426  ssidcn  21059  resthauslem  21167  sshauslem  21176  hausdiag  21448  idqtop  21509  fmid  21764  iducn  22087  mbfid  23403  dvid  23681  dvexp  23716  wilthlem2  24795  wilthlem3  24796  idmot  25432  ausgrusgrb  26060  upgrres1  26205  umgrres1  26206  usgrres1  26207  usgrexilem  26336  sizusglecusglem1  26357  pliguhgr  27338  hoif  28613  idunop  28837  idcnop  28840  elunop2  28872  fcobijfs  29501  pmtridf1o  29856  qqhre  30064  rrhre  30065  subfacp1lem4  31165  subfacp1lem5  31166  poimirlem15  33424  poimirlem22  33431  idlaut  35382  tendoidcl  36057  tendo0co2  36076  erng1r  36283  dvalveclem  36314  dva0g  36316  dvh0g  36400  mzpresrename  37313  eldioph2lem1  37323  eldioph2lem2  37324  diophren  37377  kelac2  37635  lnrfg  37689  uspgrsprfo  41756  idmgmhm  41788  funcringcsetcALTV2lem8  42043  funcringcsetclem8ALTV  42066