Definition df-f1 6492

Description: Define a one-to-one function. For equivalent definitions see dff12 6724 and dff13 7198. 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 18043. (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 6484	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6483	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5619	. . . 4 class ◡𝐹
7	6	wfun 6481	. . 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  6720  f1eq2  6721  f1eq3  6722  nff1  6723  dff12  6724  f1f  6725  f1ss  6730  f1ssr  6731  f1ssres  6732  f1cnvcnv  6734  f1cof1  6735  dff1o2  6774  f1f1orn  6780  f1imacnv  6785  f10  6802  fpropnf1  7211  nvof1o  7224  resf1extb  7874  resf1ext2b  7875  f1iun  7886  f11o  7889  f1o2ndf1  8061  tz7.48lem  8369  f1setex  8793  ssdomg  8936  domunsncan  9004  sbthlem9  9022  fodomr  9055  fodomfir  9227  fsuppcolem  9303  fsuppco  9304  enfin1ai  10295  injresinj  13735  cshinj  14762  isercolllem2  15617  isercoll  15619  ismon2  17690  isepi2  17697  isfth2  17873  fthoppc  17881  odf1o2  19537  frlmlbs  21766  f1lindf  21791  usgrislfuspgr  29244  subusgr  29346  trlf1  29753  trlres  29755  upgrf1istrl  29758  pthdivtx  29783  pthdifv  29786  spthdifv  29789  spthdep  29790  upgrwlkdvdelem  29792  upgrwlkdvde  29793  spthonepeq  29808  usgr2pth  29820  pthdlem1  29822  uspgrn2crct  29864  crctcshtrl  29879  rinvf1o  32691  swrdrndisj  33005  cycpmfvlem  33161  cycpmfv1  33162  cycpmfv2  33163  cycpmfv3  33164  cycpmcl  33165  extvfvcl  33668  madjusmdetlem4  33962  omssubadd  34432  onvf1od  35277  pthhashvtx  35298  subfacp1lem3  35352  subfacp1lem5  35354  sticksstones3  42575  diophrw  43179  f1cof1b  47513  upgrimtrls  48370  gpgprismgr4cycllem2  48560  imasubc3  49619