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

Theorem f1ofn 5267
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 5266 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5174 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5023  wf 5024  1-1-ontowf1o 5027
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f 5032  df-f1 5033  df-f1o 5035
This theorem is referenced by:  f1ofun  5268  f1odm  5270  isocnv2  5605  isoini  5611  isoselem  5613  bren  6518  en1  6570  xpen  6615  phplem4  6625  phplem4on  6637  dif1en  6649  fiintim  6693  supisolem  6757  ordiso2  6782  inresflem  6806  eldju  6813  caseinl  6836  enomnilem  6855  iseqf1olemnab  9978  hashfacen  10302  phimullem  11540
  Copyright terms: Public domain W3C validator