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-1→wf1 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