Theorem f1ofn 5614

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

Syntax hints:   → wi 4   Fn wfn 5346  ⟶wf 5347  –1-1-onto→wf1o 5350

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 5355  df-f1 5356  df-f1o 5358

This theorem is referenced by:  f1ofun  5615  f1odm  5617  isocnv2  5984  isoini  5990  isoselem  5992  bren  6982  en1  7038  en2  7064  xpen  7097  phplem4  7108  phplem4on  7121  dif1en  7135  fiintim  7190  residfi  7206  supisolem  7298  ordiso2  7325  inresflem  7350  eldju  7358  caseinl  7381  caseinr  7382  enomnilem  7428  enmkvlem  7451  enwomnilem  7459  iseqf1olemnab  10862  hashfacen  11204  fprodssdc  12272  phimullem  12918  znleval  14793  gfsump1  16859