Definition df-f1 5084

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 5076	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5075	. . 3 wff F : A --> B
6	3	ccnv 4496	. . . 4 class `' F
7	6	wfun 5073	. . 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  5279  f1eq2  5280  f1eq3  5281  nff1  5282  dff12  5283  f1f  5284  f1ss  5290  f1ssr  5291  f1ssres  5293  f1cnvcnv  5295  f1co  5296  dff1o2  5326  f1f1orn  5332  f1imacnv  5338  fun11iun  5342  f11o  5354  f10  5355  f1o2ndf1  6077  ssdomg  6624  phplem4dom  6707  sbthlemi9  6803  casefun  6920  casef1  6925  djufun  6939  exmidfodomrlemim  7002  ennnfonelemf1  11770