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

Theorem f1ofn 5443
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 5442 . 2 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
2 ffn 5347 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 14 1 (𝐹:𝐴1-1-onto𝐵𝐹 Fn 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   Fn wfn 5193  wf 5194  1-1-ontowf1o 5197
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 5202  df-f1 5203  df-f1o 5205
This theorem is referenced by:  f1ofun  5444  f1odm  5446  isocnv2  5791  isoini  5797  isoselem  5799  bren  6725  en1  6777  xpen  6823  phplem4  6833  phplem4on  6845  dif1en  6857  fiintim  6906  supisolem  6985  ordiso2  7012  inresflem  7037  eldju  7045  caseinl  7068  caseinr  7069  enomnilem  7114  enmkvlem  7137  enwomnilem  7145  iseqf1olemnab  10444  hashfacen  10771  fprodssdc  11553  phimullem  12179
  Copyright terms: Public domain W3C validator