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

Definition df-f1 5276
Description: Define a one-to-one function. For equivalent definitions see dff12 5452 and dff13 5799. 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 5268 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5267 . . 3  wff  F : A
--> B
63ccnv 4704 . . . 4  class  `' F
76wfun 5265 . . 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  5448  f1eq2  5449  f1eq3  5450  nff1  5451  dff12  5452  f1f  5453  f1ss  5458  f1ssr  5459  f1ssres  5460  f1cnvcnv  5461  f1co  5462  dff1o2  5493  f1f1orn  5499  f1imacnv  5505  fun11iun  5509  f11o  5522  f10  5523  tz7.48lem  6469  abianfp  6487  ssdomg  6923  domunsncan  6978  sbthlem9  6995  fodomr  7028  1sdom  7081  suppfif1  7165  enfin1ai  8026  isercolllem2  12155  isercoll  12157  ismon2  13653  isepi2  13660  isfth2  13805  fthoppc  13813  odf1o2  14900  nvof1o  23052  rinvf1o  23054  subfacp1lem3  23728  subfacp1lem5  23730  injrec2  25222  diophrw  26941  frlmlbs  27352  f1lindf  27395  injresinj  28215  istrl2  28337  wlkntrllem5  28349  wlkdvspthlem  28365  wlkdvspth  28366  cyclnspth  28376  eupatrl  28385  constr3trllem2  28397  4cycl4dv  28413
  Copyright terms: Public domain W3C validator