Theorem f1fn 6725

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

Syntax hints:   → wi 4   Fn wfn 6481  –1-1→wf1 6483

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 207  df-an 396  df-f 6490  df-f1 6491

This theorem is referenced by:  f1fun  6726  f1rel  6727  f1dm  6728  f1ssr  6730  f1f1orn  6779  f1elima  7204  f1eqcocnv  7242  domunsncan  9001  f1domfi2  9106  sbthfilem  9122  fodomfir  9237  marypha2  9348  infdifsn  9572  acndom  9964  dfac12lem2  10058  ackbij1  10150  fin23lem32  10257  fin1a2lem5  10317  fin1a2lem6  10318  pwfseqlem1  10571  hashf1lem1  14381  hashf1  14383  kerf1ghm  19145  odf1o2  19471  frlmlbs  21723  f1lindf  21748  2ndcdisj  23360  qtopf1  23720  clwlkclwwlklem2  29963  f1rnen  32590  erdszelem10  35192  pibt2  37410  dihfn  41267  dihcl  41269  dih1dimatlem  41328  dochocss  41365  onsucf1o  43265  cantnfub  43314  cantnfub2  43315  gricushgr  47921  grtrimap  47952