Theorem f1fn 6671

Description: A one-to-one mapping is a function on its domain. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1fn	⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem f1fn

Step	Hyp	Ref	Expression
1		f1f 6670	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6601	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6428  –1-1→wf1 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-f 6437  df-f1 6438

This theorem is referenced by:  f1fun  6672  f1rel  6673  f1dm  6674  f1dmOLD  6675  f1ssr  6677  f1f1orn  6727  f1elima  7136  f1eqcocnv  7173  f1eqcocnvOLD  7174  domunsncan  8859  f1domfi2  8968  sbthfilem  8984  marypha2  9198  infdifsn  9415  acndom  9807  dfac12lem2  9900  ackbij1  9994  fin23lem32  10100  fin1a2lem5  10160  fin1a2lem6  10161  pwfseqlem1  10414  hashf1lem1  14168  hashf1lem1OLD  14169  hashf1  14171  odf1o2  19178  kerf1ghm  19987  frlmlbs  21004  f1lindf  21029  2ndcdisj  22607  qtopf1  22967  clwlkclwwlklem2  28364  f1rnen  30964  erdszelem10  33162  pibt2  35588  dihfn  39282  dihcl  39284  dih1dimatlem  39343  dochocss  39380  isomushgr  45278