Definition df-f1 6507

Description: Define a one-to-one function. For equivalent definitions see dff12 6739 and dff13 7212. 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 18025. (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 6499	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6498	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5633	. . . 4 class ◡𝐹
7	6	wfun 6496	. . 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  6735  f1eq2  6736  f1eq3  6737  nff1  6738  dff12  6739  f1f  6740  f1ss  6745  f1ssr  6746  f1ssres  6747  f1cnvcnv  6749  f1cof1  6750  dff1o2  6789  f1f1orn  6795  f1imacnv  6800  f10  6817  fpropnf1  7225  nvof1o  7238  resf1extb  7888  resf1ext2b  7889  f1iun  7900  f11o  7903  f1o2ndf1  8076  tz7.48lem  8384  f1setex  8808  ssdomg  8951  domunsncan  9019  sbthlem9  9037  fodomr  9070  fodomfir  9242  fsuppcolem  9318  fsuppco  9319  enfin1ai  10308  injresinj  13721  cshinj  14748  isercolllem2  15603  isercoll  15605  ismon2  17672  isepi2  17679  isfth2  17855  fthoppc  17863  odf1o2  19519  frlmlbs  21769  f1lindf  21794  usgrislfuspgr  29278  subusgr  29380  trlf1  29788  trlres  29790  upgrf1istrl  29793  pthdivtx  29818  pthdifv  29821  spthdifv  29824  spthdep  29825  upgrwlkdvdelem  29827  upgrwlkdvde  29828  spthonepeq  29843  usgr2pth  29855  pthdlem1  29857  uspgrn2crct  29899  crctcshtrl  29914  rinvf1o  32726  swrdrndisj  33056  cycpmfvlem  33212  cycpmfv1  33213  cycpmfv2  33214  cycpmfv3  33215  cycpmcl  33216  extvfvcl  33719  madjusmdetlem4  34014  omssubadd  34484  onvf1od  35329  pthhashvtx  35350  subfacp1lem3  35404  subfacp1lem5  35406  sticksstones3  42547  diophrw  43145  f1cof1b  47466  upgrimtrls  48295  gpgprismgr4cycllem2  48485  imasubc3  49544