Theorem f1ofn 5643

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 5375  ⟶wf 5376  –1-1-onto→wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5384  df-f1 5385  df-f1o 5387

This theorem is used by:  f1ofun  5644  f1odm  5646  isocnv2  6021  isoini  6027  isoselem  6029  bren  7036  en1  7092  en2  7118  xpen  7151  phplem4  7162  phplem4on  7175  dif1en  7189  fiintim  7244  residfi  7260  supisolem  7355  ordiso2  7382  inresflem  7407  eldju  7415  caseinl  7438  caseinr  7439  enomnilem  7485  enmkvlem  7508  enwomnilem  7516  iseqf1olemnab  10959  hashfacen  11306  hashf1lem1  11307  fprodssdc  12382  phimullem  13032  ballotfilemsima  13317  gsump1  14247  znleval  15097