Definition df-f1 5598

Description: Define a one-to-one function. For equivalent definitions see dff12 5785 and dff13 6166. 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 5590	. 2
5	1, 2, 3	wf 5589	. . 3
6	3	ccnv 5003	. . . 4
7	6	wfun 5587	. . 3
8	5, 7	wa 369	. 2
9	4, 8	wb 184	1

This definition is referenced by:  f1eq1  5781  f1eq2  5782  f1eq3  5783  nff1  5784  dff12  5785  f1f  5786  f1ss  5791  f1ssr  5792  f1ssres  5793  f1cnvcnv  5794  f1co  5795  dff1o2  5826  f1f1orn  5832  f1imacnv  5837  f10  5852  nvof1o  6186  fun11iun  6760  f11o  6762  f1o2ndf1  6908  tz7.48lem  7125  ssdomg  7581  domunsncan  7637  sbthlem9  7655  fodomr  7688  1sdom  7742  fsuppcolem  7880  fsuppco  7881  enfin1ai  8785  injresinj  11926  isercolllem2  13488  isercoll  13490  ismon2  15129  isepi2  15136  isfth2  15284  fthoppc  15292  odf1o2  16593  frlmlbs  18831  f1lindf  18857  istrl2  24540  wlkntrllem3  24563  spthonepeq  24589  wlkdvspthlem  24609  wlkdvspth  24610  usgra2wlkspthlem1  24619  usgra2wlkspthlem2  24620  cyclnspth  24631  constr3trllem2  24651  4cycl4dv  24667  usg2wotspth  24884  2spontn0vne  24887  eupatrl  24968  rinvf1o  27472  subfacp1lem3  28626  subfacp1lem5  28628  diophrw  30692  usgra2pthspth  32351  spthdifv  32352  usgra2pth  32354