Definition df-f1 6487

Description: Define a one-to-one function. For equivalent definitions see dff12 6719 and dff13 7191. 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 6479	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6478	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5618	. . . 4 class ◡𝐹
7	6	wfun 6476	. . 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  6715  f1eq2  6716  f1eq3  6717  nff1  6718  dff12  6719  f1f  6720  f1ss  6725  f1ssr  6726  f1ssres  6727  f1cnvcnv  6729  f1cof1  6730  dff1o2  6769  f1f1orn  6775  f1imacnv  6780  f10  6797  fpropnf1  7204  nvof1o  7217  resf1extb  7867  resf1ext2b  7868  f1iun  7879  f11o  7882  f1o2ndf1  8055  tz7.48lem  8363  f1setex  8784  ssdomg  8925  domunsncan  8994  sbthlem9  9012  fodomr  9045  fodomfir  9218  fsuppcolem  9291  fsuppco  9292  enfin1ai  10278  injresinj  13691  cshinj  14717  isercolllem2  15573  isercoll  15575  ismon2  17641  isepi2  17648  isfth2  17824  fthoppc  17832  odf1o2  19452  frlmlbs  21704  f1lindf  21729  usgrislfuspgr  29132  subusgr  29234  trlf1  29642  trlres  29644  upgrf1istrl  29647  pthdivtx  29672  pthdifv  29675  spthdifv  29678  spthdep  29679  upgrwlkdvdelem  29681  upgrwlkdvde  29682  spthonepeq  29697  usgr2pth  29709  pthdlem1  29711  uspgrn2crct  29753  crctcshtrl  29768  rinvf1o  32574  swrdrndisj  32900  cycpmfvlem  33055  cycpmfv1  33056  cycpmfv2  33057  cycpmfv3  33058  cycpmcl  33059  madjusmdetlem4  33803  omssubadd  34274  onvf1od  35090  pthhashvtx  35111  subfacp1lem3  35165  subfacp1lem5  35167  sticksstones3  42131  diophrw  42742  f1cof1b  47071  upgrimtrls  47900  gpgprismgr4cycllem2  48090  imasubc3  49151