Theorem f1ofn 5620

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

Syntax hints:   → wi 4   Fn wfn 5352  ⟶wf 5353  –1-1-onto→wf1o 5356

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 5361  df-f1 5362  df-f1o 5364

This theorem is referenced by:  f1ofun  5621  f1odm  5623  isocnv2  5991  isoini  5997  isoselem  5999  bren  6996  en1  7052  en2  7078  xpen  7111  phplem4  7122  phplem4on  7135  dif1en  7149  fiintim  7204  residfi  7220  supisolem  7312  ordiso2  7339  inresflem  7364  eldju  7372  caseinl  7395  caseinr  7396  enomnilem  7442  enmkvlem  7465  enwomnilem  7473  iseqf1olemnab  10890  hashfacen  11236  fprodssdc  12305  phimullem  12951  ballotfilemsima  13207  gfsump1  14112  znleval  14931