Definition df-f1 6498

Description: Define a one-to-one function. For equivalent definitions see dff12 6730 and dff13 7202. 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 18015. (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 6490	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6489	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5624	. . . 4 class ◡𝐹
7	6	wfun 6487	. . 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  6726  f1eq2  6727  f1eq3  6728  nff1  6729  dff12  6730  f1f  6731  f1ss  6736  f1ssr  6737  f1ssres  6738  f1cnvcnv  6740  f1cof1  6741  dff1o2  6780  f1f1orn  6786  f1imacnv  6791  f10  6808  fpropnf1  7215  nvof1o  7228  resf1extb  7878  resf1ext2b  7879  f1iun  7890  f11o  7893  f1o2ndf1  8066  tz7.48lem  8374  f1setex  8798  ssdomg  8941  domunsncan  9009  sbthlem9  9027  fodomr  9060  fodomfir  9232  fsuppcolem  9308  fsuppco  9309  enfin1ai  10298  injresinj  13711  cshinj  14738  isercolllem2  15593  isercoll  15595  ismon2  17662  isepi2  17669  isfth2  17845  fthoppc  17853  odf1o2  19506  frlmlbs  21756  f1lindf  21781  usgrislfuspgr  29264  subusgr  29366  trlf1  29774  trlres  29776  upgrf1istrl  29779  pthdivtx  29804  pthdifv  29807  spthdifv  29810  spthdep  29811  upgrwlkdvdelem  29813  upgrwlkdvde  29814  spthonepeq  29829  usgr2pth  29841  pthdlem1  29843  uspgrn2crct  29885  crctcshtrl  29900  rinvf1o  32711  swrdrndisj  33041  cycpmfvlem  33196  cycpmfv1  33197  cycpmfv2  33198  cycpmfv3  33199  cycpmcl  33200  extvfvcl  33703  madjusmdetlem4  33989  omssubadd  34459  onvf1od  35303  pthhashvtx  35324  subfacp1lem3  35378  subfacp1lem5  35380  sticksstones3  42470  diophrw  43068  f1cof1b  47390  upgrimtrls  48219  gpgprismgr4cycllem2  48409  imasubc3  49468