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

Theorem f1ofo 5161
 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 5160 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 263 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4  ◡ccnv 4372  Fun wfun 4924  –onto→wfo 4928  –1-1-onto→wf1o 4929 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-3an 898  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959  df-f 4934  df-f1 4935  df-fo 4936  df-f1o 4937 This theorem is referenced by:  f1imacnv  5171  f1ococnv2  5181  fo00  5190  isoini  5485  isoselem  5487  f1opw2  5734  f1dmex  5771  bren  6259  f1oeng  6268  en1  6310  phplem4  6349  phplem4on  6360  dif1en  6368  supisolem  6412  ordiso2  6415  1fv  9098
 Copyright terms: Public domain W3C validator