Theorem f1ofn 5593

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

Syntax hints:   → wi 4   Fn wfn 5328  ⟶wf 5329  –1-1-onto→wf1o 5332

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 5337  df-f1 5338  df-f1o 5340

This theorem is referenced by:  f1ofun  5594  f1odm  5596  isocnv2  5963  isoini  5969  isoselem  5971  bren  6960  en1  7016  en2  7041  xpen  7074  phplem4  7084  phplem4on  7097  dif1en  7111  fiintim  7166  residfi  7182  supisolem  7250  ordiso2  7277  inresflem  7302  eldju  7310  caseinl  7333  caseinr  7334  enomnilem  7380  enmkvlem  7403  enwomnilem  7411  iseqf1olemnab  10807  hashfacen  11144  fprodssdc  12212  phimullem  12858  znleval  14729  gfsump1  16795