Definition df-f1 5193

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 5185	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5184	. . 3 wff F : A --> B
6	3	ccnv 4603	. . . 4 class `' F
7	6	wfun 5182	. . 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  5388  f1eq2  5389  f1eq3  5390  nff1  5391  dff12  5392  f1f  5393  f1ss  5399  f1ssr  5400  f1ssres  5402  f1cnvcnv  5404  f1co  5405  dff1o2  5437  f1f1orn  5443  f1imacnv  5449  fun11iun  5453  f11o  5465  f10  5466  f1o2ndf1  6196  ssdomg  6744  phplem4dom  6828  sbthlemi9  6930  casefun  7050  casef1  7055  djufun  7069  exmidfodomrlemim  7157  ennnfonelemf1  12351