Theorem f1fn 6550

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

Syntax hints:   → wi 4   Fn wfn 6319  –1-1→wf1 6321

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 210  df-an 400  df-f 6328  df-f1 6329

This theorem is referenced by:  f1fun  6551  f1rel  6552  f1dm  6553  f1dmOLD  6554  f1ssr  6556  f1f1orn  6601  f1elima  6999  f1eqcocnv  7035  f1eqcocnvOLD  7036  domunsncan  8600  marypha2  8887  infdifsn  9104  acndom  9462  dfac12lem2  9555  ackbij1  9649  fin23lem32  9755  fin1a2lem5  9815  fin1a2lem6  9816  pwfseqlem1  10069  hashf1lem1  13809  hashf1  13811  odf1o2  18690  kerf1ghm  19491  frlmlbs  20486  f1lindf  20511  2ndcdisj  22061  qtopf1  22421  clwlkclwwlklem2  27785  f1rnen  30388  erdszelem10  32560  pibt2  34834  dihfn  38564  dihcl  38566  dih1dimatlem  38625  dochocss  38662  isomushgr  44344