Theorem f1ofn 5433

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

Syntax hints:   → wi 4   Fn wfn 5183  ⟶wf 5184  –1-1-onto→wf1o 5187

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f 5192  df-f1 5193  df-f1o 5195

This theorem is referenced by:  f1ofun  5434  f1odm  5436  isocnv2  5780  isoini  5786  isoselem  5788  bren  6713  en1  6765  xpen  6811  phplem4  6821  phplem4on  6833  dif1en  6845  fiintim  6894  supisolem  6973  ordiso2  7000  inresflem  7025  eldju  7033  caseinl  7056  caseinr  7057  enomnilem  7102  enmkvlem  7125  enwomnilem  7133  iseqf1olemnab  10423  hashfacen  10749  fprodssdc  11531  phimullem  12157