Definition df-f1 6493

Description: Define a one-to-one function. For equivalent definitions see dff12 6725 and dff13 7201. 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 18049. (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 6485	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6484	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5619	. . . 4 class ◡𝐹
7	6	wfun 6482	. . 3 wff Fun ◡𝐹
8	5, 7	wa 397	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 208	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6721  f1eq2  6722  f1eq3  6723  nff1  6724  dff12  6725  f1f  6726  f1ss  6731  f1ssr  6732  f1ssres  6733  f1cnvcnv  6735  f1cof1  6736  dff1o2  6775  f1f1orn  6781  f1imacnv  6786  f10  6803  fpropnf1  7214  nvof1o  7227  resf1extb  7878  resf1ext2b  7879  f1iun  7888  f11o  7891  f1o2ndf1  8063  tz7.48lem  8374  f1setex  8798  ssdomg  8941  domunsncan  9009  sbthlem9  9027  fodomr  9060  fodomfir  9232  fsuppcolem  9308  fsuppco  9309  enfin1ai  10302  injresinj  13741  cshinj  14768  isercolllem2  15623  isercoll  15625  ismon2  17696  isepi2  17703  isfth2  17879  fthoppc  17887  odf1o2  19542  frlmlbs  21775  f1lindf  21800  usgrislfuspgr  29276  subusgr  29378  trlf1  29785  trlres  29787  upgrf1istrl  29790  pthdivtx  29815  pthdifv  29818  spthdifv  29821  spthdep  29822  upgrwlkdvdelem  29824  upgrwlkdvde  29825  spthonepeq  29840  usgr2pth  29852  pthdlem1  29854  uspgrn2crct  29896  crctcshtrl  29911  rinvf1o  32724  swrdrndisj  33038  cycpmfvlem  33195  cycpmfv1  33196  cycpmfv2  33197  cycpmfv3  33198  cycpmcl  33199  extvfvcl  33730  madjusmdetlem4  34024  omssubadd  34494  onvf1od  35348  pthhashvtx  35369  subfacp1lem3  35423  subfacp1lem5  35425  sticksstones3  42646  diophrw  43221  f1cof1b  47552  upgrimtrls  48409  gpgprismgr4cycllem2  48599  imasubc3  49658