Definition df-f1 5222

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 5214	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5213	. . 3 wff F : A --> B
6	3	ccnv 4626	. . . 4 class `' F
7	6	wfun 5211	. . 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  5417  f1eq2  5418  f1eq3  5419  nff1  5420  dff12  5421  f1f  5422  f1ss  5428  f1ssr  5429  f1ssres  5431  f1cnvcnv  5433  f1co  5434  dff1o2  5467  f1f1orn  5473  f1imacnv  5479  fun11iun  5483  f11o  5495  f10  5496  f1o2ndf1  6229  ssdomg  6778  phplem4dom  6862  sbthlemi9  6964  casefun  7084  casef1  7089  djufun  7103  exmidfodomrlemim  7200  ennnfonelemf1  12419