Definition df-f1 6504

Description: Define a one-to-one function. For equivalent definitions see dff12 6737 and dff13 7211. 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 6496	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6495	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5630	. . . 4 class ◡𝐹
7	6	wfun 6493	. . 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  6733  f1eq2  6734  f1eq3  6735  nff1  6736  dff12  6737  f1f  6738  f1ss  6743  f1ssr  6744  f1ssres  6745  f1cnvcnv  6747  f1cof1  6748  dff1o2  6787  f1f1orn  6793  f1imacnv  6798  f10  6815  fpropnf1  7224  nvof1o  7237  resf1extb  7890  resf1ext2b  7891  f1iun  7902  f11o  7905  f1o2ndf1  8078  tz7.48lem  8386  f1setex  8807  ssdomg  8948  domunsncan  9018  sbthlem9  9036  fodomr  9069  1sdomOLD  9172  fodomfir  9255  fsuppcolem  9328  fsuppco  9329  enfin1ai  10313  injresinj  13725  cshinj  14752  isercolllem2  15608  isercoll  15610  ismon2  17672  isepi2  17679  isfth2  17855  fthoppc  17863  odf1o2  19479  frlmlbs  21682  f1lindf  21707  usgrislfuspgr  29090  subusgr  29192  trlf1  29600  trlres  29602  upgrf1istrl  29605  pthdivtx  29630  pthdifv  29633  spthdifv  29636  spthdep  29637  upgrwlkdvdelem  29639  upgrwlkdvde  29640  spthonepeq  29655  usgr2pth  29667  pthdlem1  29669  uspgrn2crct  29711  crctcshtrl  29726  rinvf1o  32527  swrdrndisj  32852  cycpmfvlem  33042  cycpmfv1  33043  cycpmfv2  33044  cycpmfv3  33045  cycpmcl  33046  madjusmdetlem4  33793  omssubadd  34264  onvf1od  35067  pthhashvtx  35088  subfacp1lem3  35142  subfacp1lem5  35144  sticksstones3  42109  diophrw  42720  f1cof1b  47051  upgrimtrls  47879  gpgprismgr4cycllem2  48059  imasubc3  49118