Theorem f1ofn 5464

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

Syntax hints:   → wi 4   Fn wfn 5213  ⟶wf 5214  –1-1-onto→wf1o 5217

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 5222  df-f1 5223  df-f1o 5225

This theorem is referenced by:  f1ofun  5465  f1odm  5467  isocnv2  5815  isoini  5821  isoselem  5823  bren  6749  en1  6801  xpen  6847  phplem4  6857  phplem4on  6869  dif1en  6881  fiintim  6930  supisolem  7009  ordiso2  7036  inresflem  7061  eldju  7069  caseinl  7092  caseinr  7093  enomnilem  7138  enmkvlem  7161  enwomnilem  7169  iseqf1olemnab  10490  hashfacen  10818  fprodssdc  11600  phimullem  12227