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

Theorem f1ofo 5133
 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 5132 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
21simplbi 259 1 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴onto𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4  ◡ccnv 4344  Fun wfun 4896  –onto→wfo 4900  –1-1-onto→wf1o 4901 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-3an 887  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931  df-f 4906  df-f1 4907  df-fo 4908  df-f1o 4909 This theorem is referenced by:  f1imacnv  5143  f1ococnv2  5153  fo00  5162  isoini  5457  isoselem  5459  f1opw2  5706  f1dmex  5743  bren  6228  f1oeng  6237  en1  6279  phplem4  6318  phplem4on  6329  dif1en  6337  ordiso2  6357  1fv  8996
 Copyright terms: Public domain W3C validator