Definition df-f1 6542

Description: Define a one-to-one function. For equivalent definitions see dff12 6774 and dff13 7254. 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 18180. (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 6534	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6533	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5658	. . . 4 class ◡𝐹
7	6	wfun 6531	. . 3 wff Fun ◡𝐹
8	5, 7	wa 401	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 209	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is used by:  f1eq1  6770  f1eq2  6771  f1eq3  6772  nff1  6773  dff12  6774  f1f  6775  f1ss  6782  f1ssr  6783  f1ssres  6784  f1cnvcnv  6786  f1cof1  6787  dff1o2  6827  f1f1orn  6833  f1imacnv  6838  f10  6855  fpropnf1  7267  nvof1o  7284  resf1extb  7934  resf1ext2b  7935  f1iun  7944  f11o  7947  f1o2ndf1  8122  tz7.48lem  8433  f1setex  8861  ssdomg  9009  domunsncan  9078  sbthlem9  9096  fodomr  9129  fodomfir  9300  fsuppcolem  9374  fsuppco  9375  enfin1ai  10389  injresinj  13849  f1resfz0f1d  13850  cshinj  14884  isercolllem2  15755  isercoll  15757  ismon2  17827  isepi2  17834  isfth2  18010  fthoppc  18018  odf1o2  19701  frlmlbs  22011  f1lindf  22036  usgrislfuspgr  29633  subusgr  29735  trlf1  30146  trlres  30148  upgrf1istrl  30151  pthdivtx  30177  pthhashvtx  30180  pthdifv  30181  spthdifv  30184  spthdep  30185  upgrwlkdvdelem  30187  upgrwlkdvde  30188  spthonepeq  30203  usgr2pth  30215  pthdlem1  30217  uspgrn2crct  30262  crctcshtrl  30277  rinvf1o  33090  swrdrndisj  33384  cycpmfvlem  33539  cycpmfv1  33540  cycpmfv2  33541  cycpmfv3  33542  cycpmcl  33543  extvfvcl  34033  madjusmdetlem4  34327  omssubadd  34798  onvf1od  35691  subfacp1lem3  35748  subfacp1lem5  35750  sticksstones3  43001  diophrw  43591  f1cof1b  47952  upgrimtrls  48809  gpgprismgr4cycllem2  48999  imasubc3  50069  wrdf1d  50760