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

Definition df-f1 4686
Description: Define a one-to-one function. For equivalent definitions see dff12 5374 and dff13 5717. 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 4670 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4669 . . 3  wff  F : A
--> B
63ccnv 4660 . . . 4  class  `' F
76wfun 4667 . . 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  5370  f1eq2  5371  f1eq3  5372  nff1  5373  dff12  5374  f1f  5375  f1ss  5380  f1ssr  5381  f1ssres  5382  f1cnvcnv  5383  f1co  5384  dff1o2  5415  f1f1orn  5421  f1imacnv  5427  fun11iun  5431  f11o  5444  f10  5445  tz7.48lem  6421  abianfp  6439  ssdomg  6875  domunsncan  6930  sbthlem9  6947  fodomr  6980  1sdom  7033  suppfif1  7117  enfin1ai  7978  isercolllem2  12105  isercoll  12107  ismon2  13600  isepi2  13607  isfth2  13752  fthoppc  13760  odf1o2  14847  nvof1o  22998  rinvf1o  23000  subfacp1lem3  23086  subfacp1lem5  23088  injrec2  24487  diophrw  26206  frlmlbs  26617  f1lindf  26660
  Copyright terms: Public domain W3C validator