Theorem f1ofn 5532

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

Syntax hints:   → wi 4   Fn wfn 5272  ⟶wf 5273  –1-1-onto→wf1o 5276

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 5281  df-f1 5282  df-f1o 5284

This theorem is referenced by:  f1ofun  5533  f1odm  5535  isocnv2  5891  isoini  5897  isoselem  5899  bren  6845  en1  6901  en2  6923  xpen  6954  phplem4  6964  phplem4on  6976  dif1en  6988  fiintim  7040  residfi  7054  supisolem  7122  ordiso2  7149  inresflem  7174  eldju  7182  caseinl  7205  caseinr  7206  enomnilem  7252  enmkvlem  7275  enwomnilem  7283  iseqf1olemnab  10659  hashfacen  10994  fprodssdc  11951  phimullem  12597  znleval  14465