Theorem f1ofn 5481

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

Syntax hints:   → wi 4   Fn wfn 5230  ⟶wf 5231  –1-1-onto→wf1o 5234

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 5239  df-f1 5240  df-f1o 5242

This theorem is referenced by:  f1ofun  5482  f1odm  5484  isocnv2  5834  isoini  5840  isoselem  5842  bren  6774  en1  6826  xpen  6874  phplem4  6884  phplem4on  6896  dif1en  6908  fiintim  6958  supisolem  7038  ordiso2  7065  inresflem  7090  eldju  7098  caseinl  7121  caseinr  7122  enomnilem  7167  enmkvlem  7190  enwomnilem  7198  iseqf1olemnab  10521  hashfacen  10851  fprodssdc  11633  phimullem  12260