Theorem f1fn 6759

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

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

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 6517  df-f1 6518

This theorem is referenced by:  f1fun  6760  f1rel  6761  f1dm  6762  f1ssr  6764  f1f1orn  6813  f1elima  7240  f1eqcocnv  7278  domunsncan  9045  f1domfi2  9151  sbthfilem  9167  fodomfir  9285  marypha2  9396  infdifsn  9616  acndom  10010  dfac12lem2  10104  ackbij1  10196  fin23lem32  10303  fin1a2lem5  10363  fin1a2lem6  10364  pwfseqlem1  10617  hashf1lem1  14426  hashf1  14428  kerf1ghm  19185  odf1o2  19509  frlmlbs  21712  f1lindf  21737  2ndcdisj  23349  qtopf1  23709  clwlkclwwlklem2  29935  f1rnen  32559  erdszelem10  35187  pibt2  37400  dihfn  41257  dihcl  41259  dih1dimatlem  41318  dochocss  41355  onsucf1o  43254  cantnfub  43303  cantnfub2  43304  gricushgr  47907  grtrimap  47937