Definition df-f1 6567

Description: Define a one-to-one function. For equivalent definitions see dff12 6803 and dff13 7274. 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 18140. (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 6559	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6558	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5687	. . . 4 class ◡𝐹
7	6	wfun 6556	. . 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  6799  f1eq2  6800  f1eq3  6801  nff1  6802  dff12  6803  f1f  6804  f1ss  6809  f1ssr  6810  f1ssres  6811  f1cnvcnv  6813  f1cof1  6814  dff1o2  6853  f1f1orn  6859  f1imacnv  6864  f10  6881  fpropnf1  7286  nvof1o  7299  f1iun  7966  f11o  7969  f1o2ndf1  8145  tz7.48lem  8479  f1setex  8895  ssdomg  9038  domunsncan  9110  sbthlem9  9129  fodomr  9166  1sdomOLD  9282  fodomfir  9365  fsuppcolem  9438  fsuppco  9439  enfin1ai  10421  injresinj  13823  cshinj  14845  isercolllem2  15698  isercoll  15700  ismon2  17781  isepi2  17788  isfth2  17968  fthoppc  17976  odf1o2  19605  frlmlbs  21834  f1lindf  21859  usgrislfuspgr  29218  subusgr  29320  trlf1  29730  trlres  29732  upgrf1istrl  29735  pthdivtx  29761  spthdifv  29765  spthdep  29766  upgrwlkdvdelem  29768  upgrwlkdvde  29769  spthonepeq  29784  usgr2pth  29796  pthdlem1  29798  uspgrn2crct  29837  crctcshtrl  29852  rinvf1o  32646  swrdrndisj  32926  cycpmfvlem  33114  cycpmfv1  33115  cycpmfv2  33116  cycpmfv3  33117  cycpmcl  33118  madjusmdetlem4  33790  omssubadd  34281  pthhashvtx  35111  subfacp1lem3  35166  subfacp1lem5  35168  sticksstones3  42129  diophrw  42746  f1cof1b  47026