Theorem f1fn 6724

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 6723	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6656	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6480  –1-1→wf1 6482

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 208  df-an 397  df-f 6489  df-f1 6490

This theorem is referenced by:  f1fun  6725  f1rel  6726  f1dm  6727  f1ssr  6729  f1f1orn  6778  f1elima  7207  f1eqcocnv  7245  domunsncan  9005  f1domfi2  9106  sbthfilem  9122  fodomfir  9228  marypha2  9342  infdifsn  9569  acndom  9964  dfac12lem2  10058  ackbij1  10150  fin23lem32  10257  fin1a2lem5  10317  fin1a2lem6  10318  pwfseqlem1  10572  hashf1lem1  14408  hashf1  14410  kerf1ghm  19213  odf1o2  19539  frlmlbs  21772  f1lindf  21797  2ndcdisj  23439  qtopf1  23799  clwlkclwwlklem2  30088  f1rnen  32720  fineqvinfep  35306  erdszelem10  35428  pibt2  37779  dihfn  41760  dihcl  41762  dih1dimatlem  41821  dochocss  41858  onsucf1o  43717  cantnfub  43766  cantnfub2  43767  gricushgr  48408  grtrimap  48439