Definition df-f1 6578

Description: Define a one-to-one function. For equivalent definitions see dff12 6816 and dff13 7292. 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 18154. (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 6570	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6569	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5699	. . . 4 class ◡𝐹
7	6	wfun 6567	. . 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  6812  f1eq2  6813  f1eq3  6814  nff1  6815  dff12  6816  f1f  6817  f1ss  6822  f1ssr  6823  f1ssres  6824  f1cnvcnv  6826  f1cof1  6827  f1coOLD  6829  dff1o2  6867  f1f1orn  6873  f1imacnv  6878  f10  6895  fpropnf1  7304  nvof1o  7316  f1iun  7984  f11o  7987  f1o2ndf1  8163  tz7.48lem  8497  f1setex  8915  ssdomg  9060  domunsncan  9138  sbthlem9  9157  fodomr  9194  1sdomOLD  9312  fodomfir  9396  fsuppcolem  9470  fsuppco  9471  enfin1ai  10453  injresinj  13838  cshinj  14859  isercolllem2  15714  isercoll  15716  ismon2  17795  isepi2  17802  isfth2  17982  fthoppc  17990  odf1o2  19615  frlmlbs  21840  f1lindf  21865  usgrislfuspgr  29222  subusgr  29324  trlf1  29734  trlres  29736  upgrf1istrl  29739  pthdivtx  29765  spthdifv  29769  spthdep  29770  upgrwlkdvdelem  29772  upgrwlkdvde  29773  spthonepeq  29788  usgr2pth  29800  pthdlem1  29802  uspgrn2crct  29841  crctcshtrl  29856  rinvf1o  32649  swrdrndisj  32924  cycpmfvlem  33105  cycpmfv1  33106  cycpmfv2  33107  cycpmfv3  33108  cycpmcl  33109  madjusmdetlem4  33776  omssubadd  34265  pthhashvtx  35095  subfacp1lem3  35150  subfacp1lem5  35152  sticksstones3  42105  diophrw  42715  f1cof1b  46992