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

Theorem f1ofn 5336
Description: A one-to-one onto mapping is function on its domain. (Contributed by NM, 12-Dec-2003.)
Assertion
Ref Expression
f1ofn (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)

Proof of Theorem f1ofn
StepHypRef Expression
1 f1of 5335 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5242 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5088  wf 5089  1-1-ontowf1o 5092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f 5097  df-f1 5098  df-f1o 5100
This theorem is referenced by:  f1ofun  5337  f1odm  5339  isocnv2  5681  isoini  5687  isoselem  5689  bren  6609  en1  6661  xpen  6707  phplem4  6717  phplem4on  6729  dif1en  6741  fiintim  6785  supisolem  6863  ordiso2  6888  inresflem  6913  eldju  6921  caseinl  6944  caseinr  6945  enomnilem  6978  iseqf1olemnab  10229  hashfacen  10547  phimullem  11828
  Copyright terms: Public domain W3C validator