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

Theorem f1ofn 5481
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 5480 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5384 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5230  wf 5231  1-1-ontowf1o 5234
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106
This theorem depends on definitions:  df-bi 117  df-f 5239  df-f1 5240  df-f1o 5242
This theorem is referenced by:  f1ofun  5482  f1odm  5484  isocnv2  5834  isoini  5840  isoselem  5842  bren  6774  en1  6826  xpen  6874  phplem4  6884  phplem4on  6896  dif1en  6908  fiintim  6958  supisolem  7038  ordiso2  7065  inresflem  7090  eldju  7098  caseinl  7121  caseinr  7122  enomnilem  7167  enmkvlem  7190  enwomnilem  7198  iseqf1olemnab  10521  hashfacen  10851  fprodssdc  11633  phimullem  12260
  Copyright terms: Public domain W3C validator