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

Theorem f1ofn 5254
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 5253 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5161 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5010  wf 5011  1-1-ontowf1o 5014
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-f 5019  df-f1 5020  df-f1o 5022
This theorem is referenced by:  f1ofun  5255  f1odm  5257  isocnv2  5591  isoini  5597  isoselem  5599  bren  6462  en1  6514  xpen  6559  phplem4  6569  phplem4on  6581  dif1en  6593  fiintim  6637  supisolem  6701  ordiso2  6726  inresflem  6750  eldju  6757  enomnilem  6792  iseqf1olemnab  9913  hashfacen  10237  phimullem  11475
  Copyright terms: Public domain W3C validator