Theorem f1ofn 5575

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

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

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 5322  df-f1 5323  df-f1o 5325

This theorem is referenced by:  f1ofun  5576  f1odm  5578  isocnv2  5942  isoini  5948  isoselem  5950  bren  6903  en1  6959  en2  6981  xpen  7014  phplem4  7024  phplem4on  7037  dif1en  7049  fiintim  7101  residfi  7115  supisolem  7183  ordiso2  7210  inresflem  7235  eldju  7243  caseinl  7266  caseinr  7267  enomnilem  7313  enmkvlem  7336  enwomnilem  7344  iseqf1olemnab  10731  hashfacen  11066  fprodssdc  12109  phimullem  12755  znleval  14625