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

Definition df-f1 5399
Description: Define a one-to-one function. For equivalent definitions see dff12 5578 and dff13 5943. 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 5391 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5390 . . 3  wff  F : A
--> B
63ccnv 4817 . . . 4  class  `' F
76wfun 5388 . . 3  wff  Fun  `' F
85, 7wa 359 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 177 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff set class
This definition is referenced by:  f1eq1  5574  f1eq2  5575  f1eq3  5576  nff1  5577  dff12  5578  f1f  5579  f1ss  5584  f1ssr  5585  f1ssres  5586  f1cnvcnv  5587  f1co  5588  dff1o2  5619  f1f1orn  5625  f1imacnv  5631  fun11iun  5635  f11o  5648  f10  5649  tz7.48lem  6634  abianfp  6652  ssdomg  7089  domunsncan  7144  sbthlem9  7161  fodomr  7194  1sdom  7247  suppfif1  7335  enfin1ai  8197  injresinj  11127  isercolllem2  12386  isercoll  12388  ismon2  13887  isepi2  13894  isfth2  14039  fthoppc  14047  odf1o2  15134  istrl2  21402  wlkntrllem5  21417  wlkdvspthlem  21455  wlkdvspth  21456  cyclnspth  21466  constr3trllem2  21486  4cycl4dv  21502  eupatrl  21538  nvof1o  23883  rinvf1o  23885  subfacp1lem3  24647  subfacp1lem5  24649  diophrw  26508  frlmlbs  26918  f1lindf  26961
  Copyright terms: Public domain W3C validator