Definition df-f1 5276

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 5268	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5267	. . 3 wff F : A --> B
6	3	ccnv 4674	. . . 4 class `' F
7	6	wfun 5265	. . 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  5476  f1eq2  5477  f1eq3  5478  nff1  5479  dff12  5480  f1f  5481  f1ss  5487  f1ssr  5488  f1ssres  5490  f1cnvcnv  5492  f1co  5493  dff1o2  5527  f1f1orn  5533  f1imacnv  5539  fun11iun  5543  f11o  5555  f10  5556  f1o2ndf1  6314  ssdomg  6870  phplem4dom  6959  sbthlemi9  7067  casefun  7187  casef1  7192  djufun  7206  exmidfodomrlemim  7309  4sqlemffi  12719  ennnfonelemf1  12789