Definition df-f1 5263

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 5255	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5254	. . 3 wff F : A --> B
6	3	ccnv 4662	. . . 4 class `' F
7	6	wfun 5252	. . 3 wff Fun `' F
8	5, 7	wa 104	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 105	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5458  f1eq2  5459  f1eq3  5460  nff1  5461  dff12  5462  f1f  5463  f1ss  5469  f1ssr  5470  f1ssres  5472  f1cnvcnv  5474  f1co  5475  dff1o2  5509  f1f1orn  5515  f1imacnv  5521  fun11iun  5525  f11o  5537  f10  5538  f1o2ndf1  6286  ssdomg  6837  phplem4dom  6923  sbthlemi9  7031  casefun  7151  casef1  7156  djufun  7170  exmidfodomrlemim  7268  4sqlemffi  12565  ennnfonelemf1  12635