Definition df-f1 6541

Description: Define a one-to-one function. For equivalent definitions see dff12 6773 and dff13 7252. 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 18150. (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 6533	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6532	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5659	. . . 4 class ◡𝐹
7	6	wfun 6530	. . 3 wff Fun ◡𝐹
8	5, 7	wa 400	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 209	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is used by:  f1eq1  6769  f1eq2  6770  f1eq3  6771  nff1  6772  dff12  6773  f1f  6774  f1ss  6781  f1ssr  6782  f1ssres  6783  f1cnvcnv  6785  f1cof1  6786  dff1o2  6826  f1f1orn  6832  f1imacnv  6837  f10  6854  fpropnf1  7265  nvof1o  7278  resf1extb  7929  resf1ext2b  7930  f1iun  7939  f11o  7942  f1o2ndf1  8115  tz7.48lem  8426  f1setex  8852  ssdomg  8995  domunsncan  9063  sbthlem9  9081  fodomr  9114  fodomfir  9285  fsuppcolem  9359  fsuppco  9360  enfin1ai  10374  injresinj  13827  cshinj  14855  isercolllem2  15724  isercoll  15726  ismon2  17797  isepi2  17804  isfth2  17980  fthoppc  17988  odf1o2  19649  frlmlbs  21958  f1lindf  21983  usgrislfuspgr  29548  subusgr  29650  trlf1  30057  trlres  30059  upgrf1istrl  30062  pthdivtx  30087  pthdifv  30090  spthdifv  30093  spthdep  30094  upgrwlkdvdelem  30096  upgrwlkdvde  30097  spthonepeq  30112  usgr2pth  30124  pthdlem1  30126  uspgrn2crct  30168  crctcshtrl  30183  rinvf1o  32986  swrdrndisj  33286  cycpmfvlem  33441  cycpmfv1  33442  cycpmfv2  33443  cycpmfv3  33444  cycpmcl  33445  extvfvcl  33935  madjusmdetlem4  34229  omssubadd  34699  onvf1od  35599  pthhashvtx  35628  subfacp1lem3  35682  subfacp1lem5  35684  sticksstones3  42943  diophrw  43518  f1cof1b  47842  upgrimtrls  48699  gpgprismgr4cycllem2  48889  imasubc3  49962