Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1fn Structured version   Visualization version   GIF version

Theorem f1fn 6015
 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
StepHypRef Expression
1 f1f 6014 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 ffn 5958 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801 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 196  df-an 385  df-f 5808  df-f1 5809 This theorem is referenced by:  f1fun  6016  f1rel  6017  f1dm  6018  f1ssr  6020  f1f1orn  6061  f1elima  6421  f1eqcocnv  6456  domunsncan  7945  marypha2  8228  infdifsn  8437  acndom  8757  dfac12lem2  8849  ackbij1  8943  fin23lem32  9049  fin1a2lem5  9109  fin1a2lem6  9110  pwfseqlem1  9359  hashf1lem1  13096  hashf1  13098  odf1o2  17811  kerf1hrm  18566  frlmlbs  19955  f1lindf  19980  2ndcdisj  21069  qtopf1  21429  usgraedgrn  25910  usgfidegfi  26437  erdszelem10  30436  dihfn  35575  dihcl  35577  dih1dimatlem  35636  dochocss  35673  clwlkclwwlklem2  41209
 Copyright terms: Public domain W3C validator