Definition df-f1 6566

Description: Define a one-to-one function. For equivalent definitions see dff12 6803 and dff13 7275. 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 18132. (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 6558	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6557	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5684	. . . 4 class ◡𝐹
7	6	wfun 6555	. . 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  7287  nvof1o  7300  resf1extb  7956  resf1ext2b  7957  f1iun  7968  f11o  7971  f1o2ndf1  8147  tz7.48lem  8481  f1setex  8897  ssdomg  9040  domunsncan  9112  sbthlem9  9131  fodomr  9168  1sdomOLD  9285  fodomfir  9368  fsuppcolem  9441  fsuppco  9442  enfin1ai  10424  injresinj  13827  cshinj  14849  isercolllem2  15702  isercoll  15704  ismon2  17778  isepi2  17785  isfth2  17962  fthoppc  17970  odf1o2  19591  frlmlbs  21817  f1lindf  21842  usgrislfuspgr  29204  subusgr  29306  trlf1  29716  trlres  29718  upgrf1istrl  29721  pthdivtx  29747  pthdifv  29750  spthdifv  29753  spthdep  29754  upgrwlkdvdelem  29756  upgrwlkdvde  29757  spthonepeq  29772  usgr2pth  29784  pthdlem1  29786  uspgrn2crct  29828  crctcshtrl  29843  rinvf1o  32640  swrdrndisj  32942  cycpmfvlem  33132  cycpmfv1  33133  cycpmfv2  33134  cycpmfv3  33135  cycpmcl  33136  madjusmdetlem4  33829  omssubadd  34302  pthhashvtx  35133  subfacp1lem3  35187  subfacp1lem5  35189  sticksstones3  42149  diophrw  42770  f1cof1b  47089