Definition df-f1 6544

Description: Define a one-to-one function. For equivalent definitions see dff12 6778 and dff13 7259. 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 18263. (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 6536	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6535	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5650	. . . 4 class ◡𝐹
7	6	wfun 6533	. . 3 wff Fun ◡𝐹
8	5, 7	wa 401	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 209	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is used by:  f1eq1  6774  f1eq2  6775  f1eq3  6776  nff1  6777  dff12  6778  f1f  6779  f1ss  6786  f1ssr  6787  f1ssres  6788  f1cnvcnv  6790  f1cof1  6791  dff1o2  6831  f1f1orn  6837  f1imacnv  6842  f10  6859  fpropnf1  7272  nvof1o  7289  resf1extb  7947  resf1ext2b  7948  f1iun  7957  f11o  7960  f1o2ndf1  8134  tz7.48lem  8451  tz7.48lemOLD  8452  f1setex  8880  ssdomg  9028  domunsncan  9097  sbthlem9  9115  fodomr  9148  fodomfir  9320  fsuppcolem  9394  fsuppco  9395  enfin1ai  10463  injresinj  13927  f1resfz0f1d  13928  cshinj  14963  isercolllem2  15834  isercoll  15836  ismon2  17910  isepi2  17917  isfth2  18093  fthoppc  18101  odf1o2  19788  frlmlbs  22104  f1lindf  22129  usgrislfuspgr  29769  subusgr  29871  trlf1  30282  trlres  30284  upgrf1istrl  30287  pthdivtx  30313  pthhashvtx  30316  pthdifv  30317  spthdifv  30320  spthdep  30321  upgrwlkdvdelem  30323  upgrwlkdvde  30324  spthonepeq  30339  usgr2pth  30351  pthdlem1  30353  uspgrn2crct  30398  crctcshtrl  30413  rinvf1o  33225  swrdrndisj  33519  cycpmfvlem  33674  cycpmfv1  33675  cycpmfv2  33676  cycpmfv3  33677  cycpmcl  33678  extvfvcl  34169  madjusmdetlem4  34463  omssubadd  34933  f1preimaex  35714  onvf1od  35887  subfacp1lem3  35948  subfacp1lem5  35950  sticksstones3  43200  diophrw  43771  f1cof1b  48148  upgrimtrls  49005  gpgprismgr4cycllem2  49195  imasubc3  50265  wrdf1d  50941