Theorem f1ofn 5578

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

Syntax hints:   → wi 4   Fn wfn 5316  ⟶wf 5317  –1-1-onto→wf1o 5320

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 5325  df-f1 5326  df-f1o 5328

This theorem is referenced by:  f1ofun  5579  f1odm  5581  isocnv2  5945  isoini  5951  isoselem  5953  bren  6908  en1  6964  en2  6986  xpen  7019  phplem4  7029  phplem4on  7042  dif1en  7054  fiintim  7109  residfi  7123  supisolem  7191  ordiso2  7218  inresflem  7243  eldju  7251  caseinl  7274  caseinr  7275  enomnilem  7321  enmkvlem  7344  enwomnilem  7352  iseqf1olemnab  10740  hashfacen  11076  fprodssdc  12122  phimullem  12768  znleval  14638