Theorem f1ofn 5267

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

Syntax hints:   → wi 4   Fn wfn 5023  ⟶wf 5024  –1-1-onto→wf1o 5027

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-f 5032  df-f1 5033  df-f1o 5035

This theorem is referenced by:  f1ofun  5268  f1odm  5270  isocnv2  5605  isoini  5611  isoselem  5613  bren  6518  en1  6570  xpen  6615  phplem4  6625  phplem4on  6637  dif1en  6649  fiintim  6693  supisolem  6757  ordiso2  6782  inresflem  6806  eldju  6813  caseinl  6836  enomnilem  6855  iseqf1olemnab  9978  hashfacen  10302  phimullem  11540