Definition df-f1 6501

Description: Define a one-to-one function. For equivalent definitions see dff12 6733 and dff13 7206. 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 18051. (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 6493	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6492	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5627	. . . 4 class ◡𝐹
7	6	wfun 6490	. . 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  6729  f1eq2  6730  f1eq3  6731  nff1  6732  dff12  6733  f1f  6734  f1ss  6739  f1ssr  6740  f1ssres  6741  f1cnvcnv  6743  f1cof1  6744  dff1o2  6783  f1f1orn  6789  f1imacnv  6794  f10  6811  fpropnf1  7219  nvof1o  7232  resf1extb  7882  resf1ext2b  7883  f1iun  7894  f11o  7897  f1o2ndf1  8069  tz7.48lem  8377  f1setex  8801  ssdomg  8944  domunsncan  9012  sbthlem9  9030  fodomr  9063  fodomfir  9235  fsuppcolem  9311  fsuppco  9312  enfin1ai  10303  injresinj  13743  cshinj  14770  isercolllem2  15625  isercoll  15627  ismon2  17698  isepi2  17705  isfth2  17881  fthoppc  17889  odf1o2  19545  frlmlbs  21774  f1lindf  21799  usgrislfuspgr  29253  subusgr  29355  trlf1  29762  trlres  29764  upgrf1istrl  29767  pthdivtx  29792  pthdifv  29795  spthdifv  29798  spthdep  29799  upgrwlkdvdelem  29801  upgrwlkdvde  29802  spthonepeq  29817  usgr2pth  29829  pthdlem1  29831  uspgrn2crct  29873  crctcshtrl  29888  rinvf1o  32700  swrdrndisj  33014  cycpmfvlem  33170  cycpmfv1  33171  cycpmfv2  33172  cycpmfv3  33173  cycpmcl  33174  extvfvcl  33677  madjusmdetlem4  33971  omssubadd  34441  onvf1od  35286  pthhashvtx  35307  subfacp1lem3  35361  subfacp1lem5  35363  sticksstones3  42584  diophrw  43188  f1cof1b  47516  upgrimtrls  48373  gpgprismgr4cycllem2  48563  imasubc3  49622