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

Definition df-f1 5226
Description: Define a one-to-one function. For equivalent definitions see dff12 5402 and dff13 5745. 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 5218 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5217 . . 3  wff  F : A
--> B
63ccnv 4687 . . . 4  class  `' F
76wfun 5215 . . 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  5398  f1eq2  5399  f1eq3  5400  nff1  5401  dff12  5402  f1f  5403  f1ss  5408  f1ssr  5409  f1ssres  5410  f1cnvcnv  5411  f1co  5412  dff1o2  5443  f1f1orn  5449  f1imacnv  5455  fun11iun  5459  f11o  5472  f10  5473  tz7.48lem  6449  abianfp  6467  ssdomg  6903  domunsncan  6958  sbthlem9  6975  fodomr  7008  1sdom  7061  suppfif1  7145  enfin1ai  8006  isercolllem2  12135  isercoll  12137  ismon2  13633  isepi2  13640  isfth2  13785  fthoppc  13793  odf1o2  14880  nvof1o  23032  rinvf1o  23034  subfacp1lem3  23120  subfacp1lem5  23122  injrec2  24530  diophrw  26249  frlmlbs  26660  f1lindf  26703
  Copyright terms: Public domain W3C validator