Definition df-f1 5259

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 5251	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5250	. . 3 wff F : A --> B
6	3	ccnv 4658	. . . 4 class `' F
7	6	wfun 5248	. . 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  5454  f1eq2  5455  f1eq3  5456  nff1  5457  dff12  5458  f1f  5459  f1ss  5465  f1ssr  5466  f1ssres  5468  f1cnvcnv  5470  f1co  5471  dff1o2  5505  f1f1orn  5511  f1imacnv  5517  fun11iun  5521  f11o  5533  f10  5534  f1o2ndf1  6281  ssdomg  6832  phplem4dom  6918  sbthlemi9  7024  casefun  7144  casef1  7149  djufun  7163  exmidfodomrlemim  7261  4sqlemffi  12534  ennnfonelemf1  12575