Definition df-f1 6528

Description: Define a one-to-one function. For equivalent definitions see dff12 6761 and dff13 7240. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow).

A one-to-one function is also called an "injection" or an "injective function", 𝐹:𝐴–1-1→𝐵 can be read as "𝐹 is an injection from 𝐴 into 𝐵". Injections are precisely the monomorphisms in the category SetCat of sets and set functions, see setcmon 18122. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

Detailed syntax breakdown of Definition df-f1

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1 6520	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6519	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5648	. . . 4 class ◡𝐹
7	6	wfun 6517	. . 3 wff Fun ◡𝐹
8	5, 7	wa 399	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 208	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6757  f1eq2  6758  f1eq3  6759  nff1  6760  dff12  6761  f1f  6762  f1ss  6769  f1ssr  6770  f1ssres  6771  f1cnvcnv  6773  f1cof1  6774  dff1o2  6814  f1f1orn  6820  f1imacnv  6825  f10  6842  fpropnf1  7253  nvof1o  7266  resf1extb  7917  resf1ext2b  7918  f1iun  7927  f11o  7930  f1o2ndf1  8103  tz7.48lem  8414  f1setex  8840  ssdomg  8983  domunsncan  9051  sbthlem9  9069  fodomr  9102  fodomfir  9274  fsuppcolem  9349  fsuppco  9350  enfin1ai  10343  injresinj  13799  cshinj  14826  isercolllem2  15695  isercoll  15697  ismon2  17769  isepi2  17776  isfth2  17952  fthoppc  17960  odf1o2  19615  frlmlbs  21851  f1lindf  21876  usgrislfuspgr  29390  subusgr  29492  trlf1  29899  trlres  29901  upgrf1istrl  29904  pthdivtx  29929  pthdifv  29932  spthdifv  29935  spthdep  29936  upgrwlkdvdelem  29938  upgrwlkdvde  29939  spthonepeq  29954  usgr2pth  29966  pthdlem1  29968  uspgrn2crct  30010  crctcshtrl  30025  rinvf1o  32834  swrdrndisj  33137  cycpmfvlem  33294  cycpmfv1  33295  cycpmfv2  33296  cycpmfv3  33297  cycpmcl  33298  extvfvcl  33835  madjusmdetlem4  34129  omssubadd  34599  onvf1od  35454  pthhashvtx  35483  subfacp1lem3  35537  subfacp1lem5  35539  sticksstones3  42770  diophrw  43345  f1cof1b  47676  upgrimtrls  48533  gpgprismgr4cycllem2  48723  imasubc3  49782