ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-f1 Unicode version

Definition df-f1 5135
Description: Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-f1  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )

Detailed syntax breakdown of Definition df-f1
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cF . . 3  class  F
41, 2, 3wf1 5127 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5126 . . 3  wff  F : A
--> B
63ccnv 4545 . . . 4  class  `' F
76wfun 5124 . . 3  wff  Fun  `' F
85, 7wa 103 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 104 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5330  f1eq2  5331  f1eq3  5332  nff1  5333  dff12  5334  f1f  5335  f1ss  5341  f1ssr  5342  f1ssres  5344  f1cnvcnv  5346  f1co  5347  dff1o2  5379  f1f1orn  5385  f1imacnv  5391  fun11iun  5395  f11o  5407  f10  5408  f1o2ndf1  6132  ssdomg  6679  phplem4dom  6763  sbthlemi9  6860  casefun  6977  casef1  6982  djufun  6996  exmidfodomrlemim  7073  ennnfonelemf1  11965
  Copyright terms: Public domain W3C validator