Definition df-f1 5323

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 5315	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5314	. . 3 wff F : A --> B
6	3	ccnv 4718	. . . 4 class `' F
7	6	wfun 5312	. . 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  5526  f1eq2  5527  f1eq3  5528  nff1  5529  dff12  5530  f1f  5531  f1ss  5537  f1ssr  5538  f1ssres  5540  f1cnvcnv  5542  f1co  5543  dff1o2  5577  f1f1orn  5583  f1imacnv  5589  fun11iun  5593  f11o  5605  f10  5606  f1o2ndf1  6374  ssdomg  6930  phplem4dom  7023  sbthlemi9  7132  casefun  7252  casef1  7257  djufun  7271  exmidfodomrlemim  7379  4sqlemffi  12919  ennnfonelemf1  12989  usgrislfuspgrdom  15988