Theorem f1ofn 5502

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 5501	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵)
2		ffn 5404	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 14	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 5250  ⟶wf 5251  –1-1-onto→wf1o 5254

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 5259  df-f1 5260  df-f1o 5262

This theorem is referenced by:  f1ofun  5503  f1odm  5505  isocnv2  5856  isoini  5862  isoselem  5864  bren  6803  en1  6855  xpen  6903  phplem4  6913  phplem4on  6925  dif1en  6937  fiintim  6987  residfi  7001  supisolem  7069  ordiso2  7096  inresflem  7121  eldju  7129  caseinl  7152  caseinr  7153  enomnilem  7199  enmkvlem  7222  enwomnilem  7230  iseqf1olemnab  10575  hashfacen  10910  fprodssdc  11736  phimullem  12366  znleval  14152