Definition df-f1 6549

Description: Define a one-to-one function. For equivalent definitions see dff12 6787 and dff13 7254. 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 18037. (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 6541	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6540	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5676	. . . 4 class ◡𝐹
7	6	wfun 6538	. . 3 wff Fun ◡𝐹
8	5, 7	wa 397	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 205	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6783  f1eq2  6784  f1eq3  6785  nff1  6786  dff12  6787  f1f  6788  f1ss  6794  f1ssr  6795  f1ssres  6796  f1cnvcnv  6798  f1cof1  6799  f1coOLD  6801  dff1o2  6839  f1f1orn  6845  f1imacnv  6850  f10  6867  fpropnf1  7266  nvof1o  7278  f1iun  7930  f11o  7933  f1o2ndf1  8108  tz7.48lem  8441  f1setex  8851  ssdomg  8996  domunsncan  9072  sbthlem9  9091  fodomr  9128  1sdomOLD  9249  fsuppcolem  9396  fsuppco  9397  enfin1ai  10379  injresinj  13753  cshinj  14761  isercolllem2  15612  isercoll  15614  ismon2  17681  isepi2  17688  isfth2  17866  fthoppc  17874  odf1o2  19441  frlmlbs  21352  f1lindf  21377  usgrislfuspgr  28444  subusgr  28546  trlf1  28955  trlres  28957  upgrf1istrl  28960  pthdivtx  28986  spthdifv  28990  spthdep  28991  upgrwlkdvdelem  28993  upgrwlkdvde  28994  spthonepeq  29009  usgr2pth  29021  pthdlem1  29023  uspgrn2crct  29062  crctcshtrl  29077  rinvf1o  31854  swrdrndisj  32121  cycpmfvlem  32271  cycpmfv1  32272  cycpmfv2  32273  cycpmfv3  32274  cycpmcl  32275  madjusmdetlem4  32810  omssubadd  33299  pthhashvtx  34118  subfacp1lem3  34173  subfacp1lem5  34175  sticksstones3  40964  diophrw  41497  f1cof1b  45785