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

Theorem f1ofo 5295
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 5294 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 269 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4466  Fun wfun 5043  ontowfo 5047  1-1-ontowf1o 5048
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-11 1449  ax-4 1452  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077
This theorem depends on definitions:  df-bi 116  df-3an 929  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-in 3019  df-ss 3026  df-f 5053  df-f1 5054  df-fo 5055  df-f1o 5056
This theorem is referenced by:  f1imacnv  5305  f1ococnv2  5315  fo00  5324  isoini  5635  isoselem  5637  f1opw2  5888  f1dmex  5925  bren  6544  f1oeng  6554  en1  6596  mapen  6642  ssenen  6647  phplem4  6651  phplem4on  6663  dif1en  6675  fiintim  6719  fidcenumlemim  6741  supisolem  6783  ordiso2  6808  djuunr  6838  1fv  9699  hashfacen  10356  fsumf1o  10933  fisumss  10935  exmidsbthrlem  12617
  Copyright terms: Public domain W3C validator