Definition df-f1 6486

Description: Define a one-to-one function. For equivalent definitions see dff12 6718 and dff13 7188. 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 17994. (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 6478	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6477	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5613	. . . 4 class ◡𝐹
7	6	wfun 6475	. . 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  6714  f1eq2  6715  f1eq3  6716  nff1  6717  dff12  6718  f1f  6719  f1ss  6724  f1ssr  6725  f1ssres  6726  f1cnvcnv  6728  f1cof1  6729  dff1o2  6768  f1f1orn  6774  f1imacnv  6779  f10  6796  fpropnf1  7201  nvof1o  7214  resf1extb  7864  resf1ext2b  7865  f1iun  7876  f11o  7879  f1o2ndf1  8052  tz7.48lem  8360  f1setex  8781  ssdomg  8922  domunsncan  8990  sbthlem9  9008  fodomr  9041  fodomfir  9212  fsuppcolem  9285  fsuppco  9286  enfin1ai  10275  injresinj  13691  cshinj  14718  isercolllem2  15573  isercoll  15575  ismon2  17641  isepi2  17648  isfth2  17824  fthoppc  17832  odf1o2  19485  frlmlbs  21734  f1lindf  21759  usgrislfuspgr  29165  subusgr  29267  trlf1  29675  trlres  29677  upgrf1istrl  29680  pthdivtx  29705  pthdifv  29708  spthdifv  29711  spthdep  29712  upgrwlkdvdelem  29714  upgrwlkdvde  29715  spthonepeq  29730  usgr2pth  29742  pthdlem1  29744  uspgrn2crct  29786  crctcshtrl  29801  rinvf1o  32612  swrdrndisj  32938  cycpmfvlem  33081  cycpmfv1  33082  cycpmfv2  33083  cycpmfv3  33084  cycpmcl  33085  madjusmdetlem4  33843  omssubadd  34313  onvf1od  35151  pthhashvtx  35172  subfacp1lem3  35226  subfacp1lem5  35228  sticksstones3  42251  diophrw  42862  f1cof1b  47187  upgrimtrls  48016  gpgprismgr4cycllem2  48206  imasubc3  49267