Definition df-f1 5382

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 5374	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5373	. . 3 wff F : A --> B
6	3	ccnv 4773	. . . 4 class `' F
7	6	wfun 5371	. . 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 used by:  f1eq1  5593  f1eq2  5594  f1eq3  5595  nff1  5596  dff12  5597  f1f  5598  f1ss  5604  f1ssr  5605  f1ssres  5607  f1cnvcnv  5609  f1co  5610  dff1o2  5644  f1f1orn  5650  f1imacnv  5656  fun11iun  5660  f11o  5673  f10  5674  rinvf1o  6035  f1o2ndf1  6464  f1setexg  6951  ssdomg  7065  phplem4dom  7163  sbthlemi9  7282  fsuppcorn  7301  casefun  7425  casef1  7430  djufun  7444  exmidfodomrlemim  7553  4sqlemffi  13175  ennnfonelemf1  13309  usgrislfuspgrdom  16431  subusgr  16516  trlf1  16629  trlres  16631