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  7348  ordiso2  7375  inresflem  7400  eldju  7408  caseinl  7431  caseinr  7432  enomnilem  7478  enmkvlem  7501  enwomnilem  7509  iseqf1olemnab  10940  hashfacen  11286  hashf1lem1  11287  fprodssdc  12359  phimullem  13005  ballotfilemsima  13261  gsump1  14159  znleval  14990