Theorem f1ofn 5581

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

Syntax hints:   → wi 4   Fn wfn 5319  ⟶wf 5320  –1-1-onto→wf1o 5323

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 5328  df-f1 5329  df-f1o 5331

This theorem is referenced by:  f1ofun  5582  f1odm  5584  isocnv2  5948  isoini  5954  isoselem  5956  bren  6912  en1  6968  en2  6993  xpen  7026  phplem4  7036  phplem4on  7049  dif1en  7063  fiintim  7118  residfi  7133  supisolem  7201  ordiso2  7228  inresflem  7253  eldju  7261  caseinl  7284  caseinr  7285  enomnilem  7331  enmkvlem  7354  enwomnilem  7362  iseqf1olemnab  10756  hashfacen  11093  fprodssdc  12144  phimullem  12790  znleval  14660