ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1of1 GIF version

Theorem f1of1 5332
Description: A one-to-one onto mapping is a one-to-one mapping. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1of1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)

Proof of Theorem f1of1
StepHypRef Expression
1 df-f1o 5098 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 270 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  1-1wf1 5088  ontowfo 5089  1-1-ontowf1o 5090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f1o 5098
This theorem is referenced by:  f1of  5333  f1sng  5375  f1oresrab  5551  f1ocnvfvrneq  5649  isores3  5682  isoini2  5686  f1oiso  5693  f1opw2  5942  tposf12  6132  enssdom  6622  mapen  6706  ssenen  6711  phplem4  6715  phplem4on  6727  fidceq  6729  en2eqpr  6767  fiintim  6783  f1finf1o  6801  preimaf1ofi  6805  isotilem  6859  inresflem  6911  casefun  6936  endjusym  6947  dju1p1e2  7017  frec2uzled  10153  iseqf1olemnab  10212  iseqf1olemab  10213  iseqf1olemnanb  10214  hashen  10481  hashfacen  10530  negfi  10950  fisumss  11112  phimullem  11807  ctinfom  11847  hmeoopn  12386  hmeocld  12387  hmeontr  12388  hmeoimaf1o  12389
  Copyright terms: Public domain W3C validator