Theorem f1ofn 5640

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

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

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 5381  df-f1 5382  df-f1o 5384

This theorem is used by:  f1ofun  5641  f1odm  5643  isocnv2  6018  isoini  6024  isoselem  6026  bren  7030  en1  7086  en2  7112  xpen  7145  phplem4  7156  phplem4on  7169  dif1en  7183  fiintim  7238  residfi  7254  supisolem  7349  ordiso2  7376  inresflem  7401  eldju  7409  caseinl  7432  caseinr  7433  enomnilem  7479  enmkvlem  7502  enwomnilem  7510  iseqf1olemnab  10952  hashfacen  11299  hashf1lem1  11300  fprodssdc  12375  phimullem  13025  ballotfilemsima  13310  gsump1  14208  znleval  15039