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

Definition df-f1 5488
Description: Define a one-to-one function. For equivalent definitions see dff12 5667 and dff13 6033. 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 5480 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5479 . . 3  wff  F : A
--> B
63ccnv 4906 . . . 4  class  `' F
76wfun 5477 . . 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  5663  f1eq2  5664  f1eq3  5665  nff1  5666  dff12  5667  f1f  5668  f1ss  5673  f1ssr  5674  f1ssres  5675  f1cnvcnv  5676  f1co  5677  dff1o2  5708  f1f1orn  5714  f1imacnv  5720  fun11iun  5724  f11o  5737  f10  5738  f1o2ndf1  6483  tz7.48lem  6727  abianfp  6745  ssdomg  7182  domunsncan  7237  sbthlem9  7254  fodomr  7287  1sdom  7340  suppfif1  7429  enfin1ai  8295  injresinj  11231  isercolllem2  12490  isercoll  12492  ismon2  13991  isepi2  13998  isfth2  14143  fthoppc  14151  odf1o2  15238  istrl2  21569  wlkntrllem3  21592  spthonepeq  21618  wlkdvspthlem  21638  wlkdvspth  21639  cyclnspth  21649  constr3trllem2  21669  4cycl4dv  21685  eupatrl  21721  nvof1o  24071  rinvf1o  24073  subfacp1lem3  24899  subfacp1lem5  24901  diophrw  26855  frlmlbs  27264  f1lindf  27307  usgra2pthspth  28367  usgra2wlkspthlem1  28368  usgra2wlkspthlem2  28369  spthdifv  28371  usgra2pth  28373  usg2wotspth  28440  2spontn0vne  28443
  Copyright terms: Public domain W3C validator