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

Definition df-f1 4651
Description: Define a one-to-one function. For equivalent definitions see dff12 5339 and dff13 5682. 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 4635 . 2  wff  F : A -1-1-> B
51, 2, 3wf 4634 . . 3  wff  F : A
--> B
63ccnv 4625 . . . 4  class  `' F
76wfun 4632 . . 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  5335  f1eq2  5336  f1eq3  5337  nff1  5338  dff12  5339  f1f  5340  f1ss  5345  f1ssr  5346  f1ssres  5347  f1cnvcnv  5348  f1co  5349  dff1o2  5380  f1f1orn  5386  f1imacnv  5392  fun11iun  5396  f11o  5409  f10  5410  tz7.48lem  6386  abianfp  6404  ssdomg  6840  domunsncan  6895  sbthlem9  6912  fodomr  6945  1sdom  6998  suppfif1  7082  enfin1ai  7943  isercolllem2  12069  isercoll  12071  ismon2  13564  isepi2  13571  isfth2  13716  fthoppc  13724  odf1o2  14811  nvof1o  22962  rinvf1o  22964  subfacp1lem3  23050  subfacp1lem5  23052  injrec2  24451  diophrw  26170  frlmlbs  26581  f1lindf  26624
  Copyright terms: Public domain W3C validator