Definition df-f1 6495

Description: Define a one-to-one function. For equivalent definitions see dff12 6727 and dff13 7198. 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 18009. (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 6487	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6486	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5621	. . . 4 class ◡𝐹
7	6	wfun 6484	. . 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  6723  f1eq2  6724  f1eq3  6725  nff1  6726  dff12  6727  f1f  6728  f1ss  6733  f1ssr  6734  f1ssres  6735  f1cnvcnv  6737  f1cof1  6738  dff1o2  6777  f1f1orn  6783  f1imacnv  6788  f10  6805  fpropnf1  7211  nvof1o  7224  resf1extb  7874  resf1ext2b  7875  f1iun  7886  f11o  7889  f1o2ndf1  8062  tz7.48lem  8370  f1setex  8792  ssdomg  8935  domunsncan  9003  sbthlem9  9021  fodomr  9054  fodomfir  9226  fsuppcolem  9302  fsuppco  9303  enfin1ai  10292  injresinj  13705  cshinj  14732  isercolllem2  15587  isercoll  15589  ismon2  17656  isepi2  17663  isfth2  17839  fthoppc  17847  odf1o2  19500  frlmlbs  21750  f1lindf  21775  usgrislfuspgr  29209  subusgr  29311  trlf1  29719  trlres  29721  upgrf1istrl  29724  pthdivtx  29749  pthdifv  29752  spthdifv  29755  spthdep  29756  upgrwlkdvdelem  29758  upgrwlkdvde  29759  spthonepeq  29774  usgr2pth  29786  pthdlem1  29788  uspgrn2crct  29830  crctcshtrl  29845  rinvf1o  32657  swrdrndisj  32988  cycpmfvlem  33143  cycpmfv1  33144  cycpmfv2  33145  cycpmfv3  33146  cycpmcl  33147  extvfvcl  33650  madjusmdetlem4  33936  omssubadd  34406  onvf1od  35250  pthhashvtx  35271  subfacp1lem3  35325  subfacp1lem5  35327  sticksstones3  42341  diophrw  42943  f1cof1b  47265  upgrimtrls  48094  gpgprismgr4cycllem2  48284  imasubc3  49343