Definition df-f1 6543

Description: Define a one-to-one function. For equivalent definitions see dff12 6777 and dff13 7258. 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 18262. (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 6535	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 6534	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5649	. . . 4 class ◡𝐹
7	6	wfun 6532	. . 3 wff Fun ◡𝐹
8	5, 7	wa 401	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 209	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is used by:  f1eq1  6773  f1eq2  6774  f1eq3  6775  nff1  6776  dff12  6777  f1f  6778  f1ss  6785  f1ssr  6786  f1ssres  6787  f1cnvcnv  6789  f1cof1  6790  dff1o2  6830  f1f1orn  6836  f1imacnv  6841  f10  6858  fpropnf1  7271  nvof1o  7288  resf1extb  7946  resf1ext2b  7947  f1iun  7956  f11o  7959  f1o2ndf1  8133  tz7.48lem  8450  tz7.48lemOLD  8451  f1setex  8879  ssdomg  9027  domunsncan  9096  sbthlem9  9114  fodomr  9147  fodomfir  9319  fsuppcolem  9393  fsuppco  9394  enfin1ai  10462  injresinj  13926  f1resfz0f1d  13927  cshinj  14962  isercolllem2  15833  isercoll  15835  ismon2  17909  isepi2  17916  isfth2  18092  fthoppc  18100  odf1o2  19787  frlmlbs  22103  f1lindf  22128  usgrislfuspgr  29768  subusgr  29870  trlf1  30281  trlres  30283  upgrf1istrl  30286  pthdivtx  30312  pthhashvtx  30315  pthdifv  30316  spthdifv  30319  spthdep  30320  upgrwlkdvdelem  30322  upgrwlkdvde  30323  spthonepeq  30338  usgr2pth  30350  pthdlem1  30352  uspgrn2crct  30397  crctcshtrl  30412  rinvf1o  33266  swrdrndisj  33560  cycpmfvlem  33715  cycpmfv1  33716  cycpmfv2  33717  cycpmfv3  33718  cycpmcl  33719  extvfvcl  34210  madjusmdetlem4  34504  omssubadd  34974  f1preimaex  35755  onvf1od  35928  subfacp1lem3  35989  subfacp1lem5  35991  sticksstones3  43241  diophrw  43812  f1cof1b  48189  upgrimtrls  49046  gpgprismgr4cycllem2  49236  imasubc3  50306  wrdf1d  50982