Definition df-f1 6230

Description: Define a one-to-one function. For equivalent definitions see dff12 6442 and dff13 6878. 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 17176. (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 6222	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6221	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5442	. . . 4 class ◡𝐹
7	6	wfun 6219	. . 3 wff Fun ◡𝐹
8	5, 7	wa 396	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 207	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6438  f1eq2  6439  f1eq3  6440  nff1  6441  dff12  6442  f1f  6443  f1ss  6448  f1ssr  6449  f1ssres  6450  f1cnvcnv  6452  f1co  6453  dff1o2  6488  f1f1orn  6494  f1imacnv  6499  f10  6515  fpropnf1  6890  nvof1o  6902  f1iun  7501  f11o  7504  f1o2ndf1  7671  tz7.48lem  7928  ssdomg  8403  domunsncan  8464  sbthlem9  8482  fodomr  8515  1sdom  8567  fsuppcolem  8710  fsuppco  8711  enfin1ai  9652  injresinj  13008  cshinj  14009  isercolllem2  14856  isercoll  14858  ismon2  16833  isepi2  16840  isfth2  17014  fthoppc  17022  odf1o2  18428  frlmlbs  20623  f1lindf  20648  usgrislfuspgr  26652  subusgr  26754  trlf1  27165  trlres  27167  trlresOLD  27169  upgrf1istrl  27172  pthdivtx  27197  spthdifv  27201  spthdep  27202  upgrwlkdvdelem  27204  upgrwlkdvde  27205  spthonepeq  27220  usgr2pth  27232  pthdlem1  27234  uspgrn2crct  27273  crctcshtrl  27288  rinvf1o  30065  cycpmfvlem  30401  cycpmfv1  30402  cycpmfv2  30403  cycpmfv3  30404  cycpmcl  30405  madjusmdetlem4  30710  omssubadd  31175  pthhashvtx  31982  subfacp1lem3  32037  subfacp1lem5  32039  diophrw  38841