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

Definition df-f1 5262
Description: Define a one-to-one function. For equivalent definitions see dff12 5438 and dff13 5785. 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 5254 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5253 . . 3  wff  F : A
--> B
63ccnv 4690 . . . 4  class  `' F
76wfun 5251 . . 3  wff  Fun  `' F
85, 7wa 358 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 176 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5434  f1eq2  5435  f1eq3  5436  nff1  5437  dff12  5438  f1f  5439  f1ss  5444  f1ssr  5445  f1ssres  5446  f1cnvcnv  5447  f1co  5448  dff1o2  5479  f1f1orn  5485  f1imacnv  5491  fun11iun  5495  f11o  5508  f10  5509  tz7.48lem  6455  abianfp  6473  ssdomg  6909  domunsncan  6964  sbthlem9  6981  fodomr  7014  1sdom  7067  suppfif1  7151  enfin1ai  8012  isercolllem2  12141  isercoll  12143  ismon2  13639  isepi2  13646  isfth2  13791  fthoppc  13799  odf1o2  14886  nvof1o  23038  rinvf1o  23040  subfacp1lem3  23715  subfacp1lem5  23717  injrec2  25130  diophrw  26849  frlmlbs  27260  f1lindf  27303
  Copyright terms: Public domain W3C validator