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

Theorem f1ofn 5457
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 5456 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5360 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5206  wf 5207  1-1-ontowf1o 5210
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 5215  df-f1 5216  df-f1o 5218
This theorem is referenced by:  f1ofun  5458  f1odm  5460  isocnv2  5806  isoini  5812  isoselem  5814  bren  6740  en1  6792  xpen  6838  phplem4  6848  phplem4on  6860  dif1en  6872  fiintim  6921  supisolem  7000  ordiso2  7027  inresflem  7052  eldju  7060  caseinl  7083  caseinr  7084  enomnilem  7129  enmkvlem  7152  enwomnilem  7160  iseqf1olemnab  10461  hashfacen  10787  fprodssdc  11569  phimullem  12195
  Copyright terms: Public domain W3C validator