Definition df-f1 5295

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 5287	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5286	. . 3 wff F : A --> B
6	3	ccnv 4692	. . . 4 class `' F
7	6	wfun 5284	. . 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  5498  f1eq2  5499  f1eq3  5500  nff1  5501  dff12  5502  f1f  5503  f1ss  5509  f1ssr  5510  f1ssres  5512  f1cnvcnv  5514  f1co  5515  dff1o2  5549  f1f1orn  5555  f1imacnv  5561  fun11iun  5565  f11o  5577  f10  5578  f1o2ndf1  6337  ssdomg  6893  phplem4dom  6984  sbthlemi9  7093  casefun  7213  casef1  7218  djufun  7232  exmidfodomrlemim  7340  4sqlemffi  12834  ennnfonelemf1  12904