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

Theorem f1ofo 5480
Description: A one-to-one onto function is an onto function. (Contributed by NM, 28-Apr-2004.)
Assertion
Ref Expression
f1ofo (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)

Proof of Theorem f1ofo
StepHypRef Expression
1 dff1o3 5479 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 274 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4637  Fun wfun 5222  ontowfo 5226  1-1-ontowf1o 5227
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169
This theorem depends on definitions:  df-bi 117  df-3an 981  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154  df-f 5232  df-f1 5233  df-fo 5234  df-f1o 5235
This theorem is referenced by:  f1imacnv  5490  f1ococnv2  5500  fo00  5509  isoini  5832  isoselem  5834  f1opw2  6091  f1dmex  6131  bren  6761  f1oeng  6771  en1  6813  mapen  6860  ssenen  6865  phplem4  6869  phplem4on  6881  dif1en  6893  fiintim  6942  fidcenumlemim  6965  supisolem  7021  ordiso2  7048  djuunr  7079  omct  7130  ctssexmid  7162  1fv  10153  hashfacen  10830  fsumf1o  11412  fisumss  11414  fprodf1o  11610  fprodssdc  11612  ennnfonelemrn  12434  ennnfonelemnn0  12437  ennnfonelemim  12439  exmidunben  12441  ctinfomlemom  12442  ctinfom  12443  qnnen  12446  enctlem  12447  ssomct  12460  xpsfrn  12788  imasgrpf1  13007  imasrngf1  13209  imasringf1  13313  hmeontr  14109  hmeoimaf1o  14110  subctctexmid  15047  exmidsbthrlem  15067  sbthomlem  15070
  Copyright terms: Public domain W3C validator