Definition df-f1 5423

Description: Define a one-to-one function. For equivalent definitions see dff12 5605 and dff13 5971. 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 5415	. 2
5	1, 2, 3	wf 5414	. . 3
6	3	ccnv 4839	. . . 4
7	6	wfun 5412	. . 3
8	5, 7	wa 369	. 2
9	4, 8	wb 184	1

This definition is referenced by:  f1eq1  5601  f1eq2  5602  f1eq3  5603  nff1  5604  dff12  5605  f1f  5606  f1ss  5611  f1ssr  5612  f1ssres  5613  f1cnvcnv  5614  f1co  5615  dff1o2  5646  f1f1orn  5652  f1imacnv  5657  f10  5672  nvof1o  5987  fun11iun  6537  f11o  6539  f1o2ndf1  6680  tz7.48lem  6896  ssdomg  7355  domunsncan  7411  sbthlem9  7429  fodomr  7462  1sdom  7515  fsuppcolem  7650  fsuppco  7651  enfin1ai  8553  injresinj  11639  isercolllem2  13143  isercoll  13145  ismon2  14673  isepi2  14680  isfth2  14825  fthoppc  14833  odf1o2  16072  frlmlbs  18225  f1lindf  18251  istrl2  23437  wlkntrllem3  23460  spthonepeq  23486  wlkdvspthlem  23506  wlkdvspth  23507  cyclnspth  23517  constr3trllem2  23537  4cycl4dv  23553  eupatrl  23589  rinvf1o  25949  subfacp1lem3  27070  subfacp1lem5  27072  diophrw  29097  usgra2pthspth  30295  usgra2wlkspthlem1  30296  usgra2wlkspthlem2  30297  spthdifv  30299  usgra2pth  30301  usg2wotspth  30403  2spontn0vne  30406