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

Theorem f1ofo 5340
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
Assertion
Ref Expression
f1ofo  |-  ( F : A -1-1-onto-> B  ->  F : A -onto-> B )

Proof of Theorem f1ofo
StepHypRef Expression
1 dff1o3 5339 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F : A -onto-> B  /\  Fun  `' F ) )
21simplbi 270 1  |-  ( F : A -1-1-onto-> B  ->  F : A -onto-> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4506   Fun wfun 5085   -onto->wfo 5089   -1-1-onto->wf1o 5090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-3an 947  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098
This theorem is referenced by:  f1imacnv  5350  f1ococnv2  5360  fo00  5369  isoini  5685  isoselem  5687  f1opw2  5942  f1dmex  5980  bren  6607  f1oeng  6617  en1  6659  mapen  6706  ssenen  6711  phplem4  6715  phplem4on  6727  dif1en  6739  fiintim  6783  fidcenumlemim  6806  supisolem  6861  ordiso2  6886  djuunr  6917  omct  6968  ctssexmid  6990  1fv  9867  hashfacen  10530  fsumf1o  11110  fisumss  11112  ennnfonelemrn  11838  ennnfonelemnn0  11841  ennnfonelemim  11843  exmidunben  11845  ctinfomlemom  11846  ctinfom  11847  qnnen  11850  enctlem  11851  hmeontr  12388  hmeoimaf1o  12389  subctctexmid  13030  exmidsbthrlem  13051  sbthomlem  13054
  Copyright terms: Public domain W3C validator