ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  f1f GIF version

Theorem f1f 5200
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
Assertion
Ref Expression
f1f (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 5007 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 268 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4427  Fun wfun 4996  wf 4998  1-1wf1 4999
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-f1 5007
This theorem is referenced by:  f1rn  5201  f1fn  5202  f1ss  5206  f1ssres  5209  f1of  5237  dff1o5  5246  cocan1  5548  f1o2ndf1  5975  brdomg  6445  f1dom2g  6453  f1domg  6455  dom3d  6471  f1imaen2g  6490  2dom  6502  xpdom2  6527  dom0  6534  phplem4dom  6558  isinfinf  6593  infm  6600  updjudhcoinlf  6750  updjudhcoinrg  6751  casef1  6760  djudom  6766  fihashf1rn  10162
  Copyright terms: Public domain W3C validator