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

Definition df-f1 5260
Description: Define a one-to-one function. For equivalent definitions see dff12 5436 and dff13 5783. 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 5252 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5251 . . 3  wff  F : A
--> B
63ccnv 4688 . . . 4  class  `' F
76wfun 5249 . . 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  5432  f1eq2  5433  f1eq3  5434  nff1  5435  dff12  5436  f1f  5437  f1ss  5442  f1ssr  5443  f1ssres  5444  f1cnvcnv  5445  f1co  5446  dff1o2  5477  f1f1orn  5483  f1imacnv  5489  fun11iun  5493  f11o  5506  f10  5507  tz7.48lem  6453  abianfp  6471  ssdomg  6907  domunsncan  6962  sbthlem9  6979  fodomr  7012  1sdom  7065  suppfif1  7149  enfin1ai  8010  isercolllem2  12139  isercoll  12141  ismon2  13637  isepi2  13644  isfth2  13789  fthoppc  13797  odf1o2  14884  nvof1o  23036  rinvf1o  23038  subfacp1lem3  23713  subfacp1lem5  23715  injrec2  25119  diophrw  26838  frlmlbs  27249  f1lindf  27292
  Copyright terms: Public domain W3C validator