Theorem f1ofn 5501

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

Syntax hints:   → wi 4   Fn wfn 5249  ⟶wf 5250  –1-1-onto→wf1o 5253

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 5258  df-f1 5259  df-f1o 5261

This theorem is referenced by:  f1ofun  5502  f1odm  5504  isocnv2  5855  isoini  5861  isoselem  5863  bren  6801  en1  6853  xpen  6901  phplem4  6911  phplem4on  6923  dif1en  6935  fiintim  6985  residfi  6999  supisolem  7067  ordiso2  7094  inresflem  7119  eldju  7127  caseinl  7150  caseinr  7151  enomnilem  7197  enmkvlem  7220  enwomnilem  7228  iseqf1olemnab  10572  hashfacen  10907  fprodssdc  11733  phimullem  12363  znleval  14141