Theorem f1fn 6757

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

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

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 6515  df-f1 6516

This theorem is referenced by:  f1fun  6758  f1rel  6759  f1dm  6760  f1ssr  6762  f1f1orn  6811  f1elima  7238  f1eqcocnv  7276  domunsncan  9041  f1domfi2  9146  sbthfilem  9162  fodomfir  9279  marypha2  9390  infdifsn  9610  acndom  10004  dfac12lem2  10098  ackbij1  10190  fin23lem32  10297  fin1a2lem5  10357  fin1a2lem6  10358  pwfseqlem1  10611  hashf1lem1  14420  hashf1  14422  kerf1ghm  19179  odf1o2  19503  frlmlbs  21706  f1lindf  21731  2ndcdisj  23343  qtopf1  23703  clwlkclwwlklem2  29929  f1rnen  32553  erdszelem10  35187  pibt2  37405  dihfn  41262  dihcl  41264  dih1dimatlem  41323  dochocss  41360  onsucf1o  43261  cantnfub  43310  cantnfub2  43311  gricushgr  47917  grtrimap  47947