Definition df-f1 6560

Description: Define a one-to-one function. For equivalent definitions see dff12 6796 and dff13 7278. 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 18288. (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 6552	. 2 wff 𝐹:𝐴⟶1-1𝐵
5	1, 2, 3	wf 6551	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5654	. . . 4 class ◡𝐹
7	6	wfun 6549	. . 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  6792  f1eq2  6793  f1eq3  6794  nff1  6795  dff12  6796  f1f  6797  f1ss  6804  f1ssr  6805  f1ssres  6806  f1cnvcnv  6808  f1cof1  6809  dff1o2  6849  f1f1orn  6855  f1imacnv  6860  f10  6878  fpropnf1  7291  nvof1o  7308  resf1extb  7967  resf1ext2b  7968  f1iun  7977  f11o  7980  f1o2ndf1  8157  tz7.48lem  8475  tz7.48lemOLD  8476  f1setex  8904  ssdomg  9052  domunsncan  9121  sbthlem9  9139  fodomr  9172  fodomfir  9344  fsuppcolem  9417  fsuppco  9418  enfin1ai  10486  injresinj  13950  f1resfz0f1d  13951  cshinj  14987  isercolllem2  15859  isercoll  15861  ismon2  17935  isepi2  17942  isfth2  18118  fthoppc  18126  odf1o2  19814  frlmlbs  22130  f1lindf  22155  usgrislfuspgr  29795  subusgr  29897  trlf1  30308  trlres  30310  upgrf1istrl  30313  pthdivtx  30339  pthhashvtx  30342  pthdifv  30343  spthdifv  30346  spthdep  30347  upgrwlkdvdelem  30349  upgrwlkdvde  30350  spthonepeq  30365  usgr2pth  30377  pthdlem1  30379  uspgrn2crct  30424  crctcshtrl  30439  rinvf1o  33293  swrdrndisj  33585  cycpmfvlem  33740  cycpmfv1  33741  cycpmfv2  33742  cycpmfv3  33743  cycpmcl  33744  extvfvcl  34235  madjusmdetlem4  34529  omssubadd  34999  f1preimaex  35782  onvf1od  36034  subfacp1lem3  36113  subfacp1lem5  36115  sticksstones3  43389  diophrw  43961  f1cof1b  48350  upgrimtrls  49207  gpgprismgr4cycllem2  49397  imasubc3  50475  wrdf1d  51218