Definition df-f1 6360

Description: Define a one-to-one function. For equivalent definitions see dff12 6574 and dff13 7013. 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 17347. (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 6352	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6351	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5554	. . . 4 class ◡𝐹
7	6	wfun 6349	. . 3 wff Fun ◡𝐹
8	5, 7	wa 398	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 208	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6570  f1eq2  6571  f1eq3  6572  nff1  6573  dff12  6574  f1f  6575  f1ss  6580  f1ssr  6581  f1ssres  6582  f1cnvcnv  6584  f1co  6585  dff1o2  6620  f1f1orn  6626  f1imacnv  6631  f10  6647  fpropnf1  7025  nvof1o  7037  f1iun  7645  f11o  7648  f1o2ndf1  7818  tz7.48lem  8077  ssdomg  8555  domunsncan  8617  sbthlem9  8635  fodomr  8668  1sdom  8721  fsuppcolem  8864  fsuppco  8865  enfin1ai  9806  injresinj  13159  cshinj  14173  isercolllem2  15022  isercoll  15024  ismon2  17004  isepi2  17011  isfth2  17185  fthoppc  17193  odf1o2  18698  frlmlbs  20941  f1lindf  20966  usgrislfuspgr  26969  subusgr  27071  trlf1  27480  trlres  27482  upgrf1istrl  27485  pthdivtx  27510  spthdifv  27514  spthdep  27515  upgrwlkdvdelem  27517  upgrwlkdvde  27518  spthonepeq  27533  usgr2pth  27545  pthdlem1  27547  uspgrn2crct  27586  crctcshtrl  27601  rinvf1o  30375  swrdrndisj  30631  cycpmfvlem  30754  cycpmfv1  30755  cycpmfv2  30756  cycpmfv3  30757  cycpmcl  30758  madjusmdetlem4  31095  omssubadd  31558  pthhashvtx  32374  subfacp1lem3  32429  subfacp1lem5  32431  diophrw  39405