Definition df-f1 4850

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 4842	. 2 wff F :A -1-1->B
5	1, 2, 3	wf 4841	. . 3 wff F :A -->B
6	3	ccnv 4287	. . . 4 class `' F
7	6	wfun 4839	. . 3 wff Fun `' F
8	5, 7	wa 97	. 2 wff ( F :A -->B /\ Fun `' F)
9	4, 8	wb 98	1 wff ( F :A -1-1->B <-> ( F :A -->B /\ Fun `' F))

This definition is referenced by:  f1eq1  5030  f1eq2  5031  f1eq3  5032  nff1  5033  dff12  5034  f1f  5035  f1ss  5040  f1ssr  5041  f1ssres  5042  f1cnvcnv  5043  f1co  5044  dff1o2  5074  f1f1orn  5080  f1imacnv  5086  fun11iun  5090  f11o  5102  f10  5103  f1o2ndf1  5791  ssdomg  6194