Theorem f1ofn 5546

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

Syntax hints:   → wi 4   Fn wfn 5286  ⟶wf 5287  –1-1-onto→wf1o 5290

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 5295  df-f1 5296  df-f1o 5298

This theorem is referenced by:  f1ofun  5547  f1odm  5549  isocnv2  5906  isoini  5912  isoselem  5914  bren  6860  en1  6916  en2  6938  xpen  6969  phplem4  6979  phplem4on  6992  dif1en  7004  fiintim  7056  residfi  7070  supisolem  7138  ordiso2  7165  inresflem  7190  eldju  7198  caseinl  7221  caseinr  7222  enomnilem  7268  enmkvlem  7291  enwomnilem  7299  iseqf1olemnab  10685  hashfacen  11020  fprodssdc  12062  phimullem  12708  znleval  14576