Definition df-f1 6385

Description: Define a one-to-one function. For equivalent definitions see dff12 6614 and dff13 7067. 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 17593. (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 6377	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6376	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5550	. . . 4 class ◡𝐹
7	6	wfun 6374	. . 3 wff Fun ◡𝐹
8	5, 7	wa 399	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 209	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6610  f1eq2  6611  f1eq3  6612  nff1  6613  dff12  6614  f1f  6615  f1ss  6621  f1ssr  6622  f1ssres  6623  f1cnvcnv  6625  f1cof1  6626  f1coOLD  6628  dff1o2  6666  f1f1orn  6672  f1imacnv  6677  f10  6693  fpropnf1  7079  nvof1o  7091  f1iun  7717  f11o  7720  f1o2ndf1  7891  tz7.48lem  8177  f1setex  8538  ssdomg  8674  domunsncan  8745  sbthlem9  8764  fodomr  8797  1sdom  8881  fsuppcolem  9017  fsuppco  9018  enfin1ai  9998  injresinj  13363  cshinj  14376  isercolllem2  15229  isercoll  15231  ismon2  17239  isepi2  17246  isfth2  17422  fthoppc  17430  odf1o2  18962  frlmlbs  20759  f1lindf  20784  usgrislfuspgr  27275  subusgr  27377  trlf1  27786  trlres  27788  upgrf1istrl  27791  pthdivtx  27816  spthdifv  27820  spthdep  27821  upgrwlkdvdelem  27823  upgrwlkdvde  27824  spthonepeq  27839  usgr2pth  27851  pthdlem1  27853  uspgrn2crct  27892  crctcshtrl  27907  rinvf1o  30684  swrdrndisj  30949  cycpmfvlem  31098  cycpmfv1  31099  cycpmfv2  31100  cycpmfv3  31101  cycpmcl  31102  madjusmdetlem4  31494  omssubadd  31979  pthhashvtx  32802  subfacp1lem3  32857  subfacp1lem5  32859  sticksstones3  39826  diophrw  40284  f1cof1b  44241