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

Theorem f1ofn 5368
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 5367 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5272 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5118  wf 5119  1-1-ontowf1o 5122
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 5127  df-f1 5128  df-f1o 5130
This theorem is referenced by:  f1ofun  5369  f1odm  5371  isocnv2  5713  isoini  5719  isoselem  5721  bren  6641  en1  6693  xpen  6739  phplem4  6749  phplem4on  6761  dif1en  6773  fiintim  6817  supisolem  6895  ordiso2  6920  inresflem  6945  eldju  6953  caseinl  6976  caseinr  6977  enomnilem  7010  enwomnilem  7040  iseqf1olemnab  10275  hashfacen  10593  phimullem  11914
  Copyright terms: Public domain W3C validator