MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1oi Structured version   Visualization version   GIF version

Theorem f1oi 6826
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
StepHypRef Expression
1 fnresi 6634 . 2 ( I ↾ 𝐴) Fn 𝐴
2 cnvresid 6584 . . . 4 ( I ↾ 𝐴) = ( I ↾ 𝐴)
32fneq1i 6603 . . 3 (( I ↾ 𝐴) Fn 𝐴 ↔ ( I ↾ 𝐴) Fn 𝐴)
41, 3mpbir 230 . 2 ( I ↾ 𝐴) Fn 𝐴
5 dff1o4 6796 . 2 (( I ↾ 𝐴):𝐴1-1-onto𝐴 ↔ (( I ↾ 𝐴) Fn 𝐴( I ↾ 𝐴) Fn 𝐴))
61, 4, 5mpbir2an 710 1 ( I ↾ 𝐴):𝐴1-1-onto𝐴
Colors of variables: wff setvar class
Syntax hints:   I cid 5534  ccnv 5636  cres 5639   Fn wfn 6495  1-1-ontowf1o 6499
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pr 5388
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3062  df-rex 3071  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-sn 4591  df-pr 4593  df-op 4597  df-br 5110  df-opab 5172  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507
This theorem is referenced by:  f1ovi  6827  fveqf1o  7253  f1ofvswap  7256  isoid  7278  enrefg  8930  ssdomg  8946  enreffi  9136  ssdomfi  9149  ssdomfi2  9150  wdomref  9516  infxpenc  9962  pwfseqlem5  10607  fproddvdsd  16225  wunndx  17075  idfucl  17775  idffth  17828  ressffth  17833  setccatid  17978  estrccatid  18027  funcestrcsetclem7  18042  funcestrcsetclem8  18043  equivestrcsetc  18048  funcsetcestrclem7  18057  funcsetcestrclem8  18058  idmhm  18619  ielefmnd  18705  sursubmefmnd  18714  injsubmefmnd  18715  idghm  19031  idresperm  19175  islinds2  21242  lindfres  21252  lindsmm  21257  mdetunilem9  21992  ssidcn  22629  resthauslem  22737  sshauslem  22746  idqtop  23080  fmid  23334  iducn  23658  mbfid  25022  dvid  25305  dvexp  25340  wilthlem2  26441  wilthlem3  26442  idmot  27528  ausgrusgrb  28165  upgrres1  28310  umgrres1  28311  usgrres1  28312  usgrexilem  28437  sizusglecusglem1  28458  pliguhgr  29477  hoif  30745  idunop  30969  idcnop  30972  elunop2  31004  fcobijfs  31694  symgcom  31990  pmtridf1o  31999  cycpmfvlem  32017  cycpmfv3  32020  cycpmcl  32021  islinds5  32210  ellspds  32211  qqhre  32665  rrhre  32666  subfacp1lem4  33841  subfacp1lem5  33842  poimirlem15  36143  poimirlem22  36150  idlaut  38609  tendoidcl  39282  tendo0co2  39301  erng1r  39508  dvalveclem  39538  dva0g  39540  dvh0g  39624  mzpresrename  41120  eldioph2lem1  41130  eldioph2lem2  41131  diophren  41183  kelac2  41439  lnrfg  41493  fundcmpsurbijinjpreimafv  45689  fundcmpsurinjimaid  45693  isomgreqve  46107  ushrisomgr  46123  uspgrsprfo  46140  idmgmhm  46172  funcringcsetcALTV2lem8  46431  funcringcsetclem8ALTV  46454  itcovalendof  46845
  Copyright terms: Public domain W3C validator