Theorem f1ofn 5638

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

Syntax hints:   → wi 4   Fn wfn 5370  ⟶wf 5371  –1-1-onto→wf1o 5374

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 5379  df-f1 5380  df-f1o 5382

This theorem is referenced by:  f1ofun  5639  f1odm  5641  isocnv2  6012  isoini  6018  isoselem  6020  bren  7024  en1  7080  en2  7106  xpen  7139  phplem4  7150  phplem4on  7163  dif1en  7177  fiintim  7232  residfi  7248  supisolem  7342  ordiso2  7369  inresflem  7394  eldju  7402  caseinl  7425  caseinr  7426  enomnilem  7472  enmkvlem  7495  enwomnilem  7503  iseqf1olemnab  10921  hashfacen  11267  hashf1lem1  11268  fprodssdc  12340  phimullem  12986  ballotfilemsima  13242  gsump1  14140  znleval  14971