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

Definition df-f1 5549
Description: Define a one-to-one function. For equivalent definitions see dff12 5738 and dff13 6118. 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 5541 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5540 . . 3  wff  F : A
--> B
63ccnv 4795 . . . 4  class  `' F
76wfun 5538 . . 3  wff  Fun  `' F
85, 7wa 370 . 2  wff  ( F : A --> B  /\  Fun  `' F )
94, 8wb 187 1  wff  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
Colors of variables: wff setvar class
This definition is referenced by:  f1eq1  5734  f1eq2  5735  f1eq3  5736  nff1  5737  dff12  5738  f1f  5739  f1ss  5744  f1ssr  5745  f1ssres  5746  f1cnvcnv  5747  f1co  5748  dff1o2  5779  f1f1orn  5785  f1imacnv  5790  f10  5805  nvof1o  6138  fun11iun  6711  f11o  6713  f1o2ndf1  6859  tz7.48lem  7113  ssdomg  7569  domunsncan  7625  sbthlem9  7643  fodomr  7676  1sdom  7728  fsuppcolem  7867  fsuppco  7868  enfin1ai  8765  injresinj  11975  isercolllem2  13672  isercoll  13674  ismon2  15582  isepi2  15589  isfth2  15763  fthoppc  15771  odf1o2  17165  frlmlbs  19297  f1lindf  19322  istrl2  25210  wlkntrllem3  25233  spthonepeq  25259  wlkdvspthlem  25279  wlkdvspth  25280  usgra2wlkspthlem1  25289  usgra2wlkspthlem2  25290  cyclnspth  25301  constr3trllem2  25321  4cycl4dv  25337  usg2wotspth  25554  2spontn0vne  25557  eupatrl  25638  rinvf1o  28176  madjusmdetlem4  28608  omssubadd  29080  omssubaddOLD  29084  subfacp1lem3  29857  subfacp1lem5  29859  diophrw  35513  subusgr  39108  usgra2pthspth  39266  spthdifv  39267  usgra2pth  39269
  Copyright terms: Public domain W3C validator