Definition df-f1 4927

Description: Define a one-to-one function. 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 4919	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 4918	. . 3 wff F : A --> B
6	3	ccnv 4362	. . . 4 class `' F
7	6	wfun 4916	. . 3 wff Fun `' F
8	5, 7	wa 102	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 103	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5107  f1eq2  5108  f1eq3  5109  nff1  5110  dff12  5111  f1f  5112  f1ss  5117  f1ssr  5118  f1ssres  5119  f1cnvcnv  5120  f1co  5121  dff1o2  5151  f1f1orn  5157  f1imacnv  5163  fun11iun  5167  f11o  5179  f10  5180  f1o2ndf1  5869  ssdomg  6281  phplem4dom  6348