Theorem f1ofn 5584

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

Syntax hints:   → wi 4   Fn wfn 5321  ⟶wf 5322  –1-1-onto→wf1o 5325

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 5330  df-f1 5331  df-f1o 5333

This theorem is referenced by:  f1ofun  5585  f1odm  5587  isocnv2  5953  isoini  5959  isoselem  5961  bren  6917  en1  6973  en2  6998  xpen  7031  phplem4  7041  phplem4on  7054  dif1en  7068  fiintim  7123  residfi  7139  supisolem  7207  ordiso2  7234  inresflem  7259  eldju  7267  caseinl  7290  caseinr  7291  enomnilem  7337  enmkvlem  7360  enwomnilem  7368  iseqf1olemnab  10764  hashfacen  11101  fprodssdc  12156  phimullem  12802  znleval  14673  gfsump1  16712