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

Theorem f1of1 5460
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 5223 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 274 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  1-1wf1 5213  ontowfo 5214  1-1-ontowf1o 5215
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-f1o 5223
This theorem is referenced by:  f1of  5461  f1sng  5503  f1oresrab  5681  f1ocnvfvrneq  5782  isores3  5815  isoini2  5819  f1oiso  5826  f1opw2  6076  tposf12  6269  enssdom  6761  mapen  6845  ssenen  6850  phplem4  6854  phplem4on  6866  fidceq  6868  en2eqpr  6906  fiintim  6927  f1finf1o  6945  preimaf1ofi  6949  isotilem  7004  inresflem  7058  casefun  7083  endjusym  7094  dju1p1e2  7195  frec2uzled  10428  iseqf1olemnab  10487  iseqf1olemab  10488  iseqf1olemnanb  10489  hashen  10763  hashfacen  10815  negfi  11235  fisumss  11399  fprodssdc  11597  phimullem  12224  eulerthlemh  12230  ctinfom  12428  ssnnctlemct  12446  f1ocpbllem  12730  f1ovscpbl  12732  xpsff1o2  12769  eqgen  13084  hmeoopn  13747  hmeocld  13748  hmeontr  13749  hmeoimaf1o  13750  iswomninnlem  14733
  Copyright terms: Public domain W3C validator