Definition df-f1 5277

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 5269	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5268	. . 3 wff F : A --> B
6	3	ccnv 4675	. . . 4 class `' F
7	6	wfun 5266	. . 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  5478  f1eq2  5479  f1eq3  5480  nff1  5481  dff12  5482  f1f  5483  f1ss  5489  f1ssr  5490  f1ssres  5492  f1cnvcnv  5494  f1co  5495  dff1o2  5529  f1f1orn  5535  f1imacnv  5541  fun11iun  5545  f11o  5557  f10  5558  f1o2ndf1  6316  ssdomg  6872  phplem4dom  6961  sbthlemi9  7069  casefun  7189  casef1  7194  djufun  7208  exmidfodomrlemim  7311  4sqlemffi  12752  ennnfonelemf1  12822