Theorem f1fn 6779

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6535  –1-1→wf1 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6544  df-f1 6545

This theorem is used by:  f1fun  6780  f1funOLD  6781  f1relOLD  6783  f1dm  6784  f1ssr  6786  f1f1orn  6836  f1elima  7266  f1eqcocnv  7308  domunsncan  9072  f1domfi2  9173  sbthfilem  9189  fodomfir  9294  marypha2  9406  infdifsn  9633  acndom  10051  dfac12lem2  10144  ackbij1  10236  fin23lem32  10343  fin1a2lem5  10403  fin1a2lem6  10404  pwfseqlem1  10658  hashf1lem1  14510  hashf1  14512  kerf1ghm  19361  odf1o2  19687  frlmlbs  21997  f1lindf  22022  2ndcdisj  23664  qtopf1  24024  clwlkclwwlklem2  30418  f1rnen  33044  fineqvinfep  35595  vonf1wev  35649  erdszelem10  35729  pibt2  38120  dihfn  42100  dihcl  42102  dih1dimatlem  42161  dochocss  42198  onsucf1o  44057  cantnfub  44106  cantnfub2  44107  gricushgr  48740  grtrimap  48771