Definition df-f1 5506

Description: Define a one-to-one function. For equivalent definitions see dff12 5685 and dff13 6052. 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 5498	. 2
5	1, 2, 3	wf 5497	. . 3
6	3	ccnv 4918	. . . 4
7	6	wfun 5495	. . 3
8	5, 7	wa 360	. 2
9	4, 8	wb 178	1

This definition is referenced by:  f1eq1  5681  f1eq2  5682  f1eq3  5683  nff1  5684  dff12  5685  f1f  5686  f1ss  5691  f1ssr  5692  f1ssres  5693  f1cnvcnv  5694  f1co  5695  dff1o2  5726  f1f1orn  5732  f1imacnv  5738  fun11iun  5742  f11o  5755  f10  5756  f1o2ndf1  6504  tz7.48lem  6747  abianfp  6765  ssdomg  7202  domunsncan  7257  sbthlem9  7274  fodomr  7307  1sdom  7360  suppfif1  7449  enfin1ai  8315  injresinj  11251  isercolllem2  12510  isercoll  12512  ismon2  14011  isepi2  14018  isfth2  14163  fthoppc  14171  odf1o2  15258  istrl2  21589  wlkntrllem3  21612  spthonepeq  21638  wlkdvspthlem  21658  wlkdvspth  21659  cyclnspth  21669  constr3trllem2  21689  4cycl4dv  21705  eupatrl  21741  nvof1o  24088  rinvf1o  24090  subfacp1lem3  24972  subfacp1lem5  24974  diophrw  26998  frlmlbs  27405  f1lindf  27448  usgra2pthspth  28507  usgra2wlkspthlem1  28508  usgra2wlkspthlem2  28509  spthdifv  28511  usgra2pth  28513  usg2wotspth  28580  2spontn0vne  28583