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

Theorem f1ofo 5342
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 5341 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 272 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4508  Fun wfun 5087  ontowfo 5091  1-1-ontowf1o 5092
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-3an 949  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100
This theorem is referenced by:  f1imacnv  5352  f1ococnv2  5362  fo00  5371  isoini  5687  isoselem  5689  f1opw2  5944  f1dmex  5982  bren  6609  f1oeng  6619  en1  6661  mapen  6708  ssenen  6713  phplem4  6717  phplem4on  6729  dif1en  6741  fiintim  6785  fidcenumlemim  6808  supisolem  6863  ordiso2  6888  djuunr  6919  omct  6970  ctssexmid  6992  1fv  9884  hashfacen  10547  fsumf1o  11127  fisumss  11129  ennnfonelemrn  11859  ennnfonelemnn0  11862  ennnfonelemim  11864  exmidunben  11866  ctinfomlemom  11867  ctinfom  11868  qnnen  11871  enctlem  11872  hmeontr  12409  hmeoimaf1o  12410  subctctexmid  13123  exmidsbthrlem  13144  sbthomlem  13147
  Copyright terms: Public domain W3C validator