Definition df-f1 5893

Description: Define a one-to-one function. For equivalent definitions see dff12 6100 and dff13 6512. 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 16737. (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 5885	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5884	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5113	. . . 4 class ◡𝐹
7	6	wfun 5882	. . 3 wff Fun ◡𝐹
8	5, 7	wa 384	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 196	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6096  f1eq2  6097  f1eq3  6098  nff1  6099  dff12  6100  f1f  6101  f1ss  6106  f1ssr  6107  f1ssres  6108  f1cnvcnv  6109  f1co  6110  dff1o2  6142  f1f1orn  6148  f1imacnv  6153  f10  6169  fpropnf1  6524  nvof1o  6536  fun11iun  7126  f11o  7128  f1o2ndf1  7285  tz7.48lem  7536  ssdomg  8001  domunsncan  8060  sbthlem9  8078  fodomr  8111  1sdom  8163  fsuppcolem  8306  fsuppco  8307  enfin1ai  9206  injresinj  12589  cshinj  13557  isercolllem2  14396  isercoll  14398  ismon2  16394  isepi2  16401  isfth2  16575  fthoppc  16583  odf1o2  17988  frlmlbs  20136  f1lindf  20161  usgrislfuspgr  26079  subusgr  26181  trlf1  26595  trlres  26597  upgrf1istrl  26600  pthdivtx  26625  spthdifv  26629  spthdep  26630  upgrwlkdvdelem  26632  upgrwlkdvde  26633  spthonepeq  26648  usgr2pth  26660  pthdlem1  26662  uspgrn2crct  26700  crctcshtrl  26715  rinvf1o  29432  madjusmdetlem4  29896  omssubadd  30362  subfacp1lem3  31164  subfacp1lem5  31166  diophrw  37322