Definition df-f1 5331

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 5323	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5322	. . 3 wff F : A --> B
6	3	ccnv 4724	. . . 4 class `' F
7	6	wfun 5320	. . 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  5538  f1eq2  5539  f1eq3  5540  nff1  5541  dff12  5542  f1f  5543  f1ss  5549  f1ssr  5550  f1ssres  5552  f1cnvcnv  5554  f1co  5555  dff1o2  5589  f1f1orn  5595  f1imacnv  5601  fun11iun  5605  f11o  5618  f10  5619  f1o2ndf1  6396  ssdomg  6955  phplem4dom  7051  sbthlemi9  7167  casefun  7287  casef1  7292  djufun  7306  exmidfodomrlemim  7415  4sqlemffi  12990  ennnfonelemf1  13060  usgrislfuspgrdom  16068  subusgr  16153  trlf1  16266  trlres  16268