Theorem f1fn 6755

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

Syntax hints:   → wi 4   Fn wfn 6510  –1-1→wf1 6512

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 209  df-an 400  df-f 6519  df-f1 6520

This theorem is referenced by:  f1fun  6756  f1funOLD  6757  f1relOLD  6759  f1dm  6760  f1ssr  6762  f1f1orn  6812  f1elima  7241  f1eqcocnv  7279  domunsncan  9043  f1domfi2  9144  sbthfilem  9160  fodomfir  9266  marypha2  9380  infdifsn  9607  acndom  10002  dfac12lem2  10096  ackbij1  10188  fin23lem32  10296  fin1a2lem5  10356  fin1a2lem6  10357  pwfseqlem1  10611  hashf1lem1  14463  hashf1  14465  kerf1ghm  19268  odf1o2  19594  frlmlbs  21827  f1lindf  21852  2ndcdisj  23494  qtopf1  23854  clwlkclwwlklem2  30146  f1rnen  32778  fineqvinfep  35381  erdszelem10  35503  pibt2  37864  dihfn  41845  dihcl  41847  dih1dimatlem  41906  dochocss  41943  onsucf1o  43802  cantnfub  43851  cantnfub2  43852  gricushgr  48492  grtrimap  48523