Theorem f1ofn 5376

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

Step	Hyp	Ref	Expression
1		f1of 5375	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 5280	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5126  ⟶wf 5127  –1-1-onto→wf1o 5130

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 5135  df-f1 5136  df-f1o 5138

This theorem is referenced by:  f1ofun  5377  f1odm  5379  isocnv2  5721  isoini  5727  isoselem  5729  bren  6649  en1  6701  xpen  6747  phplem4  6757  phplem4on  6769  dif1en  6781  fiintim  6825  supisolem  6903  ordiso2  6928  inresflem  6953  eldju  6961  caseinl  6984  caseinr  6985  enomnilem  7018  enmkvlem  7043  enwomnilem  7050  iseqf1olemnab  10292  hashfacen  10611  phimullem  11937