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

Definition df-f1 5452
Description: Define a one-to-one function. For equivalent definitions see dff12 5631 and dff13 5997. 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 5444 . 2  wff  F : A -1-1-> B
51, 2, 3wf 5443 . . 3  wff  F : A
--> B
63ccnv 4870 . . . 4  class  `' F
76wfun 5441 . . 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  5627  f1eq2  5628  f1eq3  5629  nff1  5630  dff12  5631  f1f  5632  f1ss  5637  f1ssr  5638  f1ssres  5639  f1cnvcnv  5640  f1co  5641  dff1o2  5672  f1f1orn  5678  f1imacnv  5684  fun11iun  5688  f11o  5701  f10  5702  f1o2ndf1  6447  tz7.48lem  6691  abianfp  6709  ssdomg  7146  domunsncan  7201  sbthlem9  7218  fodomr  7251  1sdom  7304  suppfif1  7393  enfin1ai  8257  injresinj  11193  isercolllem2  12452  isercoll  12454  ismon2  13953  isepi2  13960  isfth2  14105  fthoppc  14113  odf1o2  15200  istrl2  21531  wlkntrllem3  21554  spthonepeq  21580  wlkdvspthlem  21600  wlkdvspth  21601  cyclnspth  21611  constr3trllem2  21631  4cycl4dv  21647  eupatrl  21683  nvof1o  24033  rinvf1o  24035  subfacp1lem3  24861  subfacp1lem5  24863  diophrw  26809  frlmlbs  27218  f1lindf  27261  usgra2pthspth  28259  usgra2wlkspthlem1  28260  usgra2wlkspthlem2  28261  spthdifv  28263  usgra2pth  28265  usg2wotspth  28305  2spontn0vne  28308
  Copyright terms: Public domain W3C validator