Definition df-f1 5931

Description: Define a one-to-one function. For equivalent definitions see dff12 6138 and dff13 6552. 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 16784. (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 5923	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5922	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 5142	. . . 4 class ◡𝐹
7	6	wfun 5920	. . 3 wff Fun ◡𝐹
8	5, 7	wa 383	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 196	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  6134  f1eq2  6135  f1eq3  6136  nff1  6137  dff12  6138  f1f  6139  f1ss  6144  f1ssr  6145  f1ssres  6146  f1cnvcnv  6147  f1co  6148  dff1o2  6180  f1f1orn  6186  f1imacnv  6191  f10  6207  fpropnf1  6564  nvof1o  6576  fun11iun  7168  f11o  7170  f1o2ndf1  7330  tz7.48lem  7581  ssdomg  8043  domunsncan  8101  sbthlem9  8119  fodomr  8152  1sdom  8204  fsuppcolem  8347  fsuppco  8348  enfin1ai  9244  injresinj  12629  cshinj  13603  isercolllem2  14440  isercoll  14442  ismon2  16441  isepi2  16448  isfth2  16622  fthoppc  16630  odf1o2  18034  frlmlbs  20184  f1lindf  20209  usgrislfuspgr  26124  subusgr  26226  trlf1  26651  trlres  26653  upgrf1istrl  26656  pthdivtx  26681  spthdifv  26685  spthdep  26686  upgrwlkdvdelem  26688  upgrwlkdvde  26689  spthonepeq  26704  usgr2pth  26716  pthdlem1  26718  uspgrn2crct  26756  crctcshtrl  26771  rinvf1o  29560  madjusmdetlem4  30024  omssubadd  30490  subfacp1lem3  31290  subfacp1lem5  31292  diophrw  37639