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

Theorem f1f 5335
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 5135 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
21simplbi 272 1 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4  ccnv 4545  Fun wfun 5124  wf 5126  1-1wf1 5127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105
This theorem depends on definitions:  df-bi 116  df-f1 5135
This theorem is referenced by:  f1rn  5336  f1fn  5337  f1ss  5341  f1ssres  5344  f1of  5374  dff1o5  5383  fsnd  5417  cocan1  5695  f1o2ndf1  6132  brdomg  6649  f1dom2g  6657  f1domg  6659  dom3d  6675  f1imaen2g  6694  2dom  6706  xpdom2  6732  dom0  6739  phplem4dom  6763  isinfinf  6798  infm  6805  updjudhcoinlf  6972  updjudhcoinrg  6973  casef1  6982  djudom  6985  difinfsnlem  6991  difinfsn  6992  fihashf1rn  10566  ennnfonelemrn  11966  reeff1o  12900  pwle2  13364
  Copyright terms: Public domain W3C validator