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

Definition df-f1 5422
Description: Define a one-to-one function. For equivalent definitions see dff12 5601 and dff13 5967. 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 5414 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5413 . . 3  wff  F : A
--> B
63ccnv 4840 . . . 4  class  `' F
76wfun 5411 . . 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  5597  f1eq2  5598  f1eq3  5599  nff1  5600  dff12  5601  f1f  5602  f1ss  5607  f1ssr  5608  f1ssres  5609  f1cnvcnv  5610  f1co  5611  dff1o2  5642  f1f1orn  5648  f1imacnv  5654  fun11iun  5658  f11o  5671  f10  5672  f1o2ndf1  6417  tz7.48lem  6661  abianfp  6679  ssdomg  7116  domunsncan  7171  sbthlem9  7188  fodomr  7221  1sdom  7274  suppfif1  7362  enfin1ai  8224  injresinj  11159  isercolllem2  12418  isercoll  12420  ismon2  13919  isepi2  13926  isfth2  14071  fthoppc  14079  odf1o2  15166  istrl2  21495  wlkntrllem3  21518  spthonepeq  21544  wlkdvspthlem  21564  wlkdvspth  21565  cyclnspth  21575  constr3trllem2  21595  4cycl4dv  21611  eupatrl  21647  nvof1o  23997  rinvf1o  23999  subfacp1lem3  24825  subfacp1lem5  24827  diophrw  26711  frlmlbs  27121  f1lindf  27164  usgra2pthspth  28039  usgra2wlkspthlem1  28040  usgra2wlkspthlem2  28041  spthdifv  28043  usgra2pth  28045  usg2wotspth  28085  2spontn0vne  28088
  Copyright terms: Public domain W3C validator