Definition df-f1 5443

Description: Define a one-to-one function. For equivalent definitions see dff12 5622 and dff13 5985. 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 5435	. 2
5	1, 2, 3	wf 5434	. . 3
6	3	ccnv 4861	. . . 4
7	6	wfun 5432	. . 3
8	5, 7	wa 360	. 2
9	4, 8	wb 178	1

This definition is referenced by:  f1eq1  5618  f1eq2  5619  f1eq3  5620  nff1  5621  dff12  5622  f1f  5623  f1ss  5628  f1ssr  5629  f1ssres  5630  f1cnvcnv  5631  f1co  5632  dff1o2  5663  f1f1orn  5669  f1imacnv  5674  f10  5689  fun11iun  6544  f11o  6546  f1o2ndf1  6686  tz7.48lem  6860  abianfp  6878  ssdomg  7317  domunsncan  7373  sbthlem9  7390  fodomr  7423  1sdom  7476  suppfif1  7566  enfin1ai  8435  injresinj  11488  isercolllem2  12990  isercoll  12992  ismon2  14514  isepi2  14521  isfth2  14666  fthoppc  14674  odf1o2  15816  frlmlbs  17743  istrl2  22559  wlkntrllem3  22582  spthonepeq  22608  wlkdvspthlem  22628  wlkdvspth  22629  cyclnspth  22639  constr3trllem2  22659  4cycl4dv  22675  eupatrl  22711  nvof1o  25076  rinvf1o  25078  subfacp1lem3  26216  subfacp1lem5  26218  diophrw  28245  f1lindf  28632  usgra2pthspth  29476  usgra2wlkspthlem1  29477  usgra2wlkspthlem2  29478  spthdifv  29480  usgra2pth  29482  usg2wotspth  29584  2spontn0vne  29587