Theorem f1ofn 5569

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

Syntax hints:   → wi 4   Fn wfn 5309  ⟶wf 5310  –1-1-onto→wf1o 5313

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 5318  df-f1 5319  df-f1o 5321

This theorem is referenced by:  f1ofun  5570  f1odm  5572  isocnv2  5929  isoini  5935  isoselem  5937  bren  6885  en1  6941  en2  6963  xpen  6994  phplem4  7004  phplem4on  7017  dif1en  7029  fiintim  7081  residfi  7095  supisolem  7163  ordiso2  7190  inresflem  7215  eldju  7223  caseinl  7246  caseinr  7247  enomnilem  7293  enmkvlem  7316  enwomnilem  7324  iseqf1olemnab  10710  hashfacen  11045  fprodssdc  12087  phimullem  12733  znleval  14602