Theorem f1fn 6728

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

Syntax hints:   → wi 4   Fn wfn 6484  –1-1→wf1 6486

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 6493  df-f1 6494

This theorem is referenced by:  f1fun  6729  f1rel  6730  f1dm  6731  f1ssr  6733  f1f1orn  6782  f1elima  7206  f1eqcocnv  7244  domunsncan  9001  f1domfi2  9102  sbthfilem  9118  fodomfir  9223  marypha2  9334  infdifsn  9558  acndom  9953  dfac12lem2  10047  ackbij1  10139  fin23lem32  10246  fin1a2lem5  10306  fin1a2lem6  10307  pwfseqlem1  10560  hashf1lem1  14369  hashf1  14371  kerf1ghm  19167  odf1o2  19493  frlmlbs  21743  f1lindf  21768  2ndcdisj  23391  qtopf1  23751  clwlkclwwlklem2  30001  f1rnen  32632  erdszelem10  35316  pibt2  37534  dihfn  41440  dihcl  41442  dih1dimatlem  41501  dochocss  41538  onsucf1o  43429  cantnfub  43478  cantnfub2  43479  gricushgr  48079  grtrimap  48110