Definition df-f1 6546

Description: Define a one-to-one function. For equivalent definitions see dff12 6784 and dff13 7251. 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 18034. (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 6538	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6537	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5675	. . . 4 class ◡𝐹
7	6	wfun 6535	. . 3 wff Fun ◡𝐹
8	5, 7	wa 397	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 205	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6780  f1eq2  6781  f1eq3  6782  nff1  6783  dff12  6784  f1f  6785  f1ss  6791  f1ssr  6792  f1ssres  6793  f1cnvcnv  6795  f1cof1  6796  f1coOLD  6798  dff1o2  6836  f1f1orn  6842  f1imacnv  6847  f10  6864  fpropnf1  7263  nvof1o  7275  f1iun  7927  f11o  7930  f1o2ndf1  8105  tz7.48lem  8438  f1setex  8848  ssdomg  8993  domunsncan  9069  sbthlem9  9088  fodomr  9125  1sdomOLD  9246  fsuppcolem  9393  fsuppco  9394  enfin1ai  10376  injresinj  13750  cshinj  14758  isercolllem2  15609  isercoll  15611  ismon2  17678  isepi2  17685  isfth2  17863  fthoppc  17871  odf1o2  19436  frlmlbs  21344  f1lindf  21369  usgrislfuspgr  28434  subusgr  28536  trlf1  28945  trlres  28947  upgrf1istrl  28950  pthdivtx  28976  spthdifv  28980  spthdep  28981  upgrwlkdvdelem  28983  upgrwlkdvde  28984  spthonepeq  28999  usgr2pth  29011  pthdlem1  29013  uspgrn2crct  29052  crctcshtrl  29067  rinvf1o  31842  swrdrndisj  32109  cycpmfvlem  32259  cycpmfv1  32260  cycpmfv2  32261  cycpmfv3  32262  cycpmcl  32263  madjusmdetlem4  32799  omssubadd  33288  pthhashvtx  34107  subfacp1lem3  34162  subfacp1lem5  34164  sticksstones3  40953  diophrw  41483  f1cof1b  45772