Definition df-f1 5187

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 5179	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5178	. . 3 wff F : A --> B
6	3	ccnv 4597	. . . 4 class `' F
7	6	wfun 5176	. . 3 wff Fun `' F
8	5, 7	wa 103	. 2 wff ( F : A --> B /\ Fun `' F )
9	4, 8	wb 104	1 wff ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )

This definition is referenced by:  f1eq1  5382  f1eq2  5383  f1eq3  5384  nff1  5385  dff12  5386  f1f  5387  f1ss  5393  f1ssr  5394  f1ssres  5396  f1cnvcnv  5398  f1co  5399  dff1o2  5431  f1f1orn  5437  f1imacnv  5443  fun11iun  5447  f11o  5459  f10  5460  f1o2ndf1  6187  ssdomg  6735  phplem4dom  6819  sbthlemi9  6921  casefun  7041  casef1  7046  djufun  7060  exmidfodomrlemim  7148  ennnfonelemf1  12288