Theorem f1ofn 5643

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 5375  ⟶wf 5376  –1-1-onto→wf1o 5379

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-f 5384  df-f1 5385  df-f1o 5387

This theorem is used by:  f1ofun  5644  f1odm  5646  isocnv2  6021  isoini  6027  isoselem  6029  bren  7035  en1  7091  en2  7117  xpen  7150  phplem4  7161  phplem4on  7174  dif1en  7188  fiintim  7243  residfi  7259  supisolem  7355  ordiso2  7382  inresflem  7407  eldju  7415  caseinl  7438  caseinr  7439  enomnilem  7485  enmkvlem  7508  enwomnilem  7516  iseqf1olemnab  10960  hashfacen  11307  hashf1lem1  11308  fprodssdc  12383  phimullem  13033  ballotfilemsima  13318  gsump1  14248  znleval  15098