Definition df-f1 5586

Description: Define a one-to-one function. For equivalent definitions see dff12 5773 and dff13 6147. 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	|- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

Detailed syntax breakdown of Definition df-f1

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1 5578	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5577	. . 3 wff F : A --> B
6	3	ccnv 4993	. . . 4 class `' F
7	6	wfun 5575	. . 3 wff Fun `' F
8	5, 7	wa 369	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 184	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5769  f1eq2  5770  f1eq3  5771  nff1  5772  dff12  5773  f1f  5774  f1ss  5779  f1ssr  5780  f1ssres  5781  f1cnvcnv  5782  f1co  5783  dff1o2  5814  f1f1orn  5820  f1imacnv  5825  f10  5840  nvof1o  6167  fun11iun  6736  f11o  6738  f1o2ndf1  6883  tz7.48lem  7098  ssdomg  7553  domunsncan  7609  sbthlem9  7627  fodomr  7660  1sdom  7714  fsuppcolem  7851  fsuppco  7852  enfin1ai  8755  injresinj  11885  isercolllem2  13439  isercoll  13441  ismon2  14981  isepi2  14988  isfth2  15133  fthoppc  15141  odf1o2  16384  frlmlbs  18593  f1lindf  18619  istrl2  24204  wlkntrllem3  24227  spthonepeq  24253  wlkdvspthlem  24273  wlkdvspth  24274  usgra2wlkspthlem1  24283  usgra2wlkspthlem2  24284  cyclnspth  24295  constr3trllem2  24315  4cycl4dv  24331  usg2wotspth  24548  2spontn0vne  24551  eupatrl  24632  rinvf1o  27133  subfacp1lem3  28254  subfacp1lem5  28256  diophrw  30285  usgra2pthspth  31777  spthdifv  31778  usgra2pth  31780