Theorem f1ofn 5508

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

Syntax hints:   → wi 4   Fn wfn 5254  ⟶wf 5255  –1-1-onto→wf1o 5258

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 5263  df-f1 5264  df-f1o 5266

This theorem is referenced by:  f1ofun  5509  f1odm  5511  isocnv2  5862  isoini  5868  isoselem  5870  bren  6815  en1  6867  xpen  6915  phplem4  6925  phplem4on  6937  dif1en  6949  fiintim  7001  residfi  7015  supisolem  7083  ordiso2  7110  inresflem  7135  eldju  7143  caseinl  7166  caseinr  7167  enomnilem  7213  enmkvlem  7236  enwomnilem  7244  iseqf1olemnab  10610  hashfacen  10945  fprodssdc  11772  phimullem  12418  znleval  14285