Definition df-f1 6541

Description: Define a one-to-one function. For equivalent definitions see dff12 6773 and dff13 7252. 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 18143. (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 6533	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6532	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5660	. . . 4 class ◡𝐹
7	6	wfun 6530	. . 3 wff Fun ◡𝐹
8	5, 7	wa 400	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 209	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6769  f1eq2  6770  f1eq3  6771  nff1  6772  dff12  6773  f1f  6774  f1ss  6781  f1ssr  6782  f1ssres  6783  f1cnvcnv  6785  f1cof1  6786  dff1o2  6826  f1f1orn  6832  f1imacnv  6837  f10  6854  fpropnf1  7265  nvof1o  7278  resf1extb  7930  resf1ext2b  7931  f1iun  7940  f11o  7943  f1o2ndf1  8116  tz7.48lem  8427  f1setex  8853  ssdomg  8996  domunsncan  9064  sbthlem9  9082  fodomr  9115  fodomfir  9286  fsuppcolem  9360  fsuppco  9361  enfin1ai  10367  injresinj  13819  cshinj  14847  isercolllem2  15716  isercoll  15718  ismon2  17790  isepi2  17797  isfth2  17973  fthoppc  17981  odf1o2  19642  frlmlbs  21926  f1lindf  21951  usgrislfuspgr  29503  subusgr  29605  trlf1  30012  trlres  30014  upgrf1istrl  30017  pthdivtx  30042  pthdifv  30045  spthdifv  30048  spthdep  30049  upgrwlkdvdelem  30051  upgrwlkdvde  30052  spthonepeq  30067  usgr2pth  30079  pthdlem1  30081  uspgrn2crct  30123  crctcshtrl  30138  rinvf1o  32941  swrdrndisj  33243  cycpmfvlem  33398  cycpmfv1  33399  cycpmfv2  33400  cycpmfv3  33401  cycpmcl  33402  extvfvcl  33892  madjusmdetlem4  34186  omssubadd  34656  onvf1od  35545  pthhashvtx  35574  subfacp1lem3  35628  subfacp1lem5  35630  sticksstones3  42861  diophrw  43438  f1cof1b  47759  upgrimtrls  48616  gpgprismgr4cycllem2  48806  imasubc3  49879