Definition df-f1 6442

Description: Define a one-to-one function. For equivalent definitions see dff12 6678 and dff13 7137. 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 17811. (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 6434	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6433	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5589	. . . 4 class ◡𝐹
7	6	wfun 6431	. . 3 wff Fun ◡𝐹
8	5, 7	wa 396	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 205	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6674  f1eq2  6675  f1eq3  6676  nff1  6677  dff12  6678  f1f  6679  f1ss  6685  f1ssr  6686  f1ssres  6687  f1cnvcnv  6689  f1cof1  6690  f1coOLD  6692  dff1o2  6730  f1f1orn  6736  f1imacnv  6741  f10  6758  fpropnf1  7149  nvof1o  7161  f1iun  7795  f11o  7798  f1o2ndf1  7972  tz7.48lem  8281  f1setex  8654  ssdomg  8795  domunsncan  8868  sbthlem9  8887  fodomr  8924  1sdom  9034  fsuppcolem  9169  fsuppco  9170  enfin1ai  10149  injresinj  13517  cshinj  14533  isercolllem2  15386  isercoll  15388  ismon2  17455  isepi2  17462  isfth2  17640  fthoppc  17648  odf1o2  19187  frlmlbs  21013  f1lindf  21038  usgrislfuspgr  27563  subusgr  27665  trlf1  28075  trlres  28077  upgrf1istrl  28080  pthdivtx  28106  spthdifv  28110  spthdep  28111  upgrwlkdvdelem  28113  upgrwlkdvde  28114  spthonepeq  28129  usgr2pth  28141  pthdlem1  28143  uspgrn2crct  28182  crctcshtrl  28197  rinvf1o  30974  swrdrndisj  31238  cycpmfvlem  31388  cycpmfv1  31389  cycpmfv2  31390  cycpmfv3  31391  cycpmcl  31392  madjusmdetlem4  31789  omssubadd  32276  pthhashvtx  33098  subfacp1lem3  33153  subfacp1lem5  33155  sticksstones3  40111  diophrw  40588  f1cof1b  44580