Definition df-f1 6532

Description: Define a one-to-one function. For equivalent definitions see dff12 6765 and dff13 7246. 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 18223. (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 6524	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6523	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5646	. . . 4 class ◡𝐹
7	6	wfun 6521	. . 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  6761  f1eq2  6762  f1eq3  6763  nff1  6764  dff12  6765  f1f  6766  f1ss  6773  f1ssr  6774  f1ssres  6775  f1cnvcnv  6777  f1cof1  6778  dff1o2  6818  f1f1orn  6824  f1imacnv  6829  f10  6846  fpropnf1  7259  nvof1o  7276  resf1extb  7929  resf1ext2b  7930  f1iun  7939  f11o  7942  f1o2ndf1  8116  tz7.48lem  8428  tz7.48lemOLD  8429  f1setex  8857  ssdomg  9005  domunsncan  9074  sbthlem9  9092  fodomr  9125  fodomfir  9297  fsuppcolem  9371  fsuppco  9372  enfin1ai  10433  injresinj  13894  f1resfz0f1d  13895  cshinj  14929  isercolllem2  15800  isercoll  15802  ismon2  17870  isepi2  17877  isfth2  18053  fthoppc  18061  odf1o2  19748  frlmlbs  22064  f1lindf  22089  usgrislfuspgr  29701  subusgr  29803  trlf1  30214  trlres  30216  upgrf1istrl  30219  pthdivtx  30245  pthhashvtx  30248  pthdifv  30249  spthdifv  30252  spthdep  30253  upgrwlkdvdelem  30255  upgrwlkdvde  30256  spthonepeq  30271  usgr2pth  30283  pthdlem1  30285  uspgrn2crct  30330  crctcshtrl  30345  rinvf1o  33157  swrdrndisj  33451  cycpmfvlem  33606  cycpmfv1  33607  cycpmfv2  33608  cycpmfv3  33609  cycpmcl  33610  extvfvcl  34101  madjusmdetlem4  34395  omssubadd  34866  onvf1od  35811  subfacp1lem3  35868  subfacp1lem5  35870  sticksstones3  43118  diophrw  43708  f1cof1b  48069  upgrimtrls  48926  gpgprismgr4cycllem2  49116  imasubc3  50186  wrdf1d  50862