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

Theorem f1fn 6576
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 6575 . 2 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
21ffnd 6506 1 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6335  1-1wf1 6337
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 6344  df-f1 6345
This theorem is referenced by:  f1fun  6577  f1rel  6578  f1dm  6579  f1dmOLD  6580  f1ssr  6582  f1f1orn  6630  f1elima  7033  f1eqcocnv  7069  f1eqcocnvOLD  7070  domunsncan  8667  marypha2  8977  infdifsn  9194  acndom  9552  dfac12lem2  9645  ackbij1  9739  fin23lem32  9845  fin1a2lem5  9905  fin1a2lem6  9906  pwfseqlem1  10159  hashf1lem1  13907  hashf1lem1OLD  13908  hashf1  13910  odf1o2  18817  kerf1ghm  19618  frlmlbs  20614  f1lindf  20639  2ndcdisj  22208  qtopf1  22568  clwlkclwwlklem2  27937  f1rnen  30538  erdszelem10  32733  pibt2  35208  dihfn  38902  dihcl  38904  dih1dimatlem  38963  dochocss  39000  isomushgr  44804
  Copyright terms: Public domain W3C validator