Definition df-f1 5395

Description: Define a one-to-one function. For equivalent definitions see dff12 5575 and dff13 5939. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1

Detailed syntax breakdown of Definition df-f1

Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3		cF	. . 3
4	1, 2, 3	wf1 5387	. 2
5	1, 2, 3	wf 5386	. . 3
6	3	ccnv 4810	. . . 4
7	6	wfun 5384	. . 3
8	5, 7	wa 362	. 2
9	4, 8	wb 178	1

This definition is referenced by:  f1eq1  5571  f1eq2  5572  f1eq3  5573  nff1  5574  dff12  5575  f1f  5576  f1ss  5581  f1ssr  5582  f1ssres  5583  f1cnvcnv  5584  f1co  5585  dff1o2  5616  f1f1orn  5622  f1imacnv  5627  f10  5642  nvof1o  5955  fun11iun  6506  f11o  6508  f1o2ndf1  6649  tz7.48lem  6855  abianfp  6873  ssdomg  7314  domunsncan  7370  sbthlem9  7388  fodomr  7421  1sdom  7474  suppfif1  7598  fsuppco  7599  enfin1ai  8500  injresinj  11580  isercolllem2  13084  isercoll  13086  ismon2  14613  isepi2  14620  isfth2  14765  fthoppc  14773  odf1o2  16009  frlmlbs  17925  f1lindf  17950  istrl2  23116  wlkntrllem3  23139  spthonepeq  23165  wlkdvspthlem  23185  wlkdvspth  23186  cyclnspth  23196  constr3trllem2  23216  4cycl4dv  23232  eupatrl  23268  rinvf1o  25629  subfacp1lem3  26773  subfacp1lem5  26775  diophrw  28770  usgra2pthspth  29969  usgra2wlkspthlem1  29970  usgra2wlkspthlem2  29971  spthdifv  29973  usgra2pth  29975  usg2wotspth  30077  2spontn0vne  30080