Definition df-f1 6503

Description: Define a one-to-one function. For equivalent definitions see dff12 6735 and dff13 7209. 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 18054. (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 6495	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6494	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5630	. . . 4 class ◡𝐹
7	6	wfun 6492	. . 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  6731  f1eq2  6732  f1eq3  6733  nff1  6734  dff12  6735  f1f  6736  f1ss  6741  f1ssr  6742  f1ssres  6743  f1cnvcnv  6745  f1cof1  6746  dff1o2  6785  f1f1orn  6791  f1imacnv  6796  f10  6813  fpropnf1  7222  nvof1o  7235  resf1extb  7885  resf1ext2b  7886  f1iun  7897  f11o  7900  f1o2ndf1  8072  tz7.48lem  8380  f1setex  8804  ssdomg  8947  domunsncan  9015  sbthlem9  9033  fodomr  9066  fodomfir  9238  fsuppcolem  9314  fsuppco  9315  enfin1ai  10306  injresinj  13746  cshinj  14773  isercolllem2  15628  isercoll  15630  ismon2  17701  isepi2  17708  isfth2  17884  fthoppc  17892  odf1o2  19548  frlmlbs  21777  f1lindf  21802  usgrislfuspgr  29256  subusgr  29358  trlf1  29765  trlres  29767  upgrf1istrl  29770  pthdivtx  29795  pthdifv  29798  spthdifv  29801  spthdep  29802  upgrwlkdvdelem  29804  upgrwlkdvde  29805  spthonepeq  29820  usgr2pth  29832  pthdlem1  29834  uspgrn2crct  29876  crctcshtrl  29891  rinvf1o  32703  swrdrndisj  33017  cycpmfvlem  33173  cycpmfv1  33174  cycpmfv2  33175  cycpmfv3  33176  cycpmcl  33177  extvfvcl  33680  madjusmdetlem4  33974  omssubadd  34444  onvf1od  35289  pthhashvtx  35310  subfacp1lem3  35364  subfacp1lem5  35366  sticksstones3  42587  diophrw  43191  f1cof1b  47525  upgrimtrls  48382  gpgprismgr4cycllem2  48572  imasubc3  49631