Definition df-f1 6423

Description: Define a one-to-one function. For equivalent definitions see dff12 6653 and dff13 7109. 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 17718. (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 6415	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6414	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5579	. . . 4 class ◡𝐹
7	6	wfun 6412	. . 3 wff Fun ◡𝐹
8	5, 7	wa 395	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 205	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6649  f1eq2  6650  f1eq3  6651  nff1  6652  dff12  6653  f1f  6654  f1ss  6660  f1ssr  6661  f1ssres  6662  f1cnvcnv  6664  f1cof1  6665  f1coOLD  6667  dff1o2  6705  f1f1orn  6711  f1imacnv  6716  f10  6732  fpropnf1  7121  nvof1o  7133  f1iun  7760  f11o  7763  f1o2ndf1  7934  tz7.48lem  8242  f1setex  8603  ssdomg  8741  domunsncan  8812  sbthlem9  8831  fodomr  8864  1sdom  8955  fsuppcolem  9090  fsuppco  9091  enfin1ai  10071  injresinj  13436  cshinj  14452  isercolllem2  15305  isercoll  15307  ismon2  17363  isepi2  17370  isfth2  17547  fthoppc  17555  odf1o2  19093  frlmlbs  20914  f1lindf  20939  usgrislfuspgr  27457  subusgr  27559  trlf1  27968  trlres  27970  upgrf1istrl  27973  pthdivtx  27998  spthdifv  28002  spthdep  28003  upgrwlkdvdelem  28005  upgrwlkdvde  28006  spthonepeq  28021  usgr2pth  28033  pthdlem1  28035  uspgrn2crct  28074  crctcshtrl  28089  rinvf1o  30866  swrdrndisj  31131  cycpmfvlem  31281  cycpmfv1  31282  cycpmfv2  31283  cycpmfv3  31284  cycpmcl  31285  madjusmdetlem4  31682  omssubadd  32167  pthhashvtx  32989  subfacp1lem3  33044  subfacp1lem5  33046  sticksstones3  40032  diophrw  40497  f1cof1b  44456