Definition df-f1 6535

Description: Define a one-to-one function. For equivalent definitions see dff12 6772 and dff13 7246. 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 18098. (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 6527	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6526	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5653	. . . 4 class ◡𝐹
7	6	wfun 6524	. . 3 wff Fun ◡𝐹
8	5, 7	wa 395	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 206	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6768  f1eq2  6769  f1eq3  6770  nff1  6771  dff12  6772  f1f  6773  f1ss  6778  f1ssr  6779  f1ssres  6780  f1cnvcnv  6782  f1cof1  6783  dff1o2  6822  f1f1orn  6828  f1imacnv  6833  f10  6850  fpropnf1  7259  nvof1o  7272  resf1extb  7928  resf1ext2b  7929  f1iun  7940  f11o  7943  f1o2ndf1  8119  tz7.48lem  8453  f1setex  8869  ssdomg  9012  domunsncan  9084  sbthlem9  9103  fodomr  9140  1sdomOLD  9255  fodomfir  9338  fsuppcolem  9411  fsuppco  9412  enfin1ai  10396  injresinj  13802  cshinj  14827  isercolllem2  15680  isercoll  15682  ismon2  17745  isepi2  17752  isfth2  17928  fthoppc  17936  odf1o2  19552  frlmlbs  21755  f1lindf  21780  usgrislfuspgr  29112  subusgr  29214  trlf1  29624  trlres  29626  upgrf1istrl  29629  pthdivtx  29655  pthdifv  29658  spthdifv  29661  spthdep  29662  upgrwlkdvdelem  29664  upgrwlkdvde  29665  spthonepeq  29680  usgr2pth  29692  pthdlem1  29694  uspgrn2crct  29736  crctcshtrl  29751  rinvf1o  32554  swrdrndisj  32879  cycpmfvlem  33069  cycpmfv1  33070  cycpmfv2  33071  cycpmfv3  33072  cycpmcl  33073  madjusmdetlem4  33807  omssubadd  34278  pthhashvtx  35096  subfacp1lem3  35150  subfacp1lem5  35152  sticksstones3  42107  diophrw  42729  f1cof1b  47054  upgrimtrls  47867  gpgprismgr4cycllem2  48043  imasubc3  49044