Definition df-f1 6516

Description: Define a one-to-one function. For equivalent definitions see dff12 6755 and dff13 7229. 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 18049. (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 6508	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6507	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5637	. . . 4 class ◡𝐹
7	6	wfun 6505	. . 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  6751  f1eq2  6752  f1eq3  6753  nff1  6754  dff12  6755  f1f  6756  f1ss  6761  f1ssr  6762  f1ssres  6763  f1cnvcnv  6765  f1cof1  6766  dff1o2  6805  f1f1orn  6811  f1imacnv  6816  f10  6833  fpropnf1  7242  nvof1o  7255  resf1extb  7910  resf1ext2b  7911  f1iun  7922  f11o  7925  f1o2ndf1  8101  tz7.48lem  8409  f1setex  8830  ssdomg  8971  domunsncan  9041  sbthlem9  9059  fodomr  9092  1sdomOLD  9196  fodomfir  9279  fsuppcolem  9352  fsuppco  9353  enfin1ai  10337  injresinj  13749  cshinj  14776  isercolllem2  15632  isercoll  15634  ismon2  17696  isepi2  17703  isfth2  17879  fthoppc  17887  odf1o2  19503  frlmlbs  21706  f1lindf  21731  usgrislfuspgr  29114  subusgr  29216  trlf1  29626  trlres  29628  upgrf1istrl  29631  pthdivtx  29657  pthdifv  29660  spthdifv  29663  spthdep  29664  upgrwlkdvdelem  29666  upgrwlkdvde  29667  spthonepeq  29682  usgr2pth  29694  pthdlem1  29696  uspgrn2crct  29738  crctcshtrl  29753  rinvf1o  32554  swrdrndisj  32879  cycpmfvlem  33069  cycpmfv1  33070  cycpmfv2  33071  cycpmfv3  33072  cycpmcl  33073  madjusmdetlem4  33820  omssubadd  34291  onvf1od  35094  pthhashvtx  35115  subfacp1lem3  35169  subfacp1lem5  35171  sticksstones3  42136  diophrw  42747  f1cof1b  47078  upgrimtrls  47906  gpgprismgr4cycllem2  48086  imasubc3  49145