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

Theorem f1of1 5236
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 5009 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴1-1𝐵𝐹:𝐴onto𝐵))
21simplbi 268 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴1-1𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  1-1wf1 4999  ontowfo 5000  1-1-ontowf1o 5001
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-f1o 5009
This theorem is referenced by:  f1of  5237  f1oresrab  5447  f1ocnvfvrneq  5543  isores3  5576  isoini2  5580  f1oiso  5587  f1opw2  5832  tposf12  6016  enssdom  6459  mapen  6542  ssenen  6547  phplem4  6551  phplem4on  6563  fidceq  6565  en2eqpr  6603  f1finf1o  6635  preimaf1ofi  6639  isotilem  6680  inresflem  6731  casefun  6755  dju1p1e2  6802  frec2uzled  9801  iseqf1olemnab  9882  iseqf1olemab  9883  iseqf1olemnanb  9884  hashen  10157  hashfacen  10206  negfi  10623  fisumss  10748  phimullem  11283
  Copyright terms: Public domain W3C validator