Definition df-f1 5359

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 5351	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5350	. . 3 wff F : A --> B
6	3	ccnv 4750	. . . 4 class `' F
7	6	wfun 5348	. . 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  5570  f1eq2  5571  f1eq3  5572  nff1  5573  dff12  5574  f1f  5575  f1ss  5581  f1ssr  5582  f1ssres  5584  f1cnvcnv  5586  f1co  5587  dff1o2  5621  f1f1orn  5627  f1imacnv  5633  fun11iun  5637  f11o  5650  f10  5651  f1o2ndf1  6426  ssdomg  7020  phplem4dom  7118  sbthlemi9  7237  fsuppcorn  7256  casefun  7378  casef1  7383  djufun  7397  exmidfodomrlemim  7506  4sqlemffi  13098  ennnfonelemf1  13186  usgrislfuspgrdom  16202  subusgr  16287  trlf1  16400  trlres  16402