MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-f1 Unicode version

Definition df-f1 4605
Description: Define a one-to-one function. For equivalent definitions see dff12 5293 and dff13 5635. 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 4589 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4588 . . 3  wff  F : A
--> B
63ccnv 4579 . . . 4  class  `' F
76wfun 4586 . . 3  wff  Fun  `' F
85, 7wa 360 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 178 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5289  f1eq2  5290  f1eq3  5291  nff1  5292  dff12  5293  f1f  5294  f1ss  5299  f1ssr  5300  f1ssres  5301  f1cnvcnv  5302  f1co  5303  dff1o2  5334  f1f1orn  5340  f1imacnv  5346  fun11iun  5350  f11o  5363  f10  5364  tz7.48lem  6339  abianfp  6357  ssdomg  6793  domunsncan  6847  sbthlem9  6864  fodomr  6897  1sdom  6950  suppfif1  7033  enfin1ai  7894  isercolllem2  12016  isercoll  12018  ismon2  13481  isepi2  13488  isfth2  13633  fthoppc  13641  odf1o2  14719  subfacp1lem3  22884  subfacp1lem5  22886  injrec2  24285  diophrw  26004  frlmlbs  26415  f1lindf  26458
  Copyright terms: Public domain W3C validator