Definition df-f1 5338

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 5330	. 2 wff F : A -1-1-> B
5	1, 2, 3	wf 5329	. . 3 wff F : A --> B
6	3	ccnv 4730	. . . 4 class `' F
7	6	wfun 5327	. . 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  5546  f1eq2  5547  f1eq3  5548  nff1  5549  dff12  5550  f1f  5551  f1ss  5557  f1ssr  5558  f1ssres  5560  f1cnvcnv  5562  f1co  5563  dff1o2  5597  f1f1orn  5603  f1imacnv  5609  fun11iun  5613  f11o  5626  f10  5627  f1o2ndf1  6402  ssdomg  6995  phplem4dom  7091  sbthlemi9  7207  casefun  7327  casef1  7332  djufun  7346  exmidfodomrlemim  7455  4sqlemffi  13032  ennnfonelemf1  13102  usgrislfuspgrdom  16114  subusgr  16199  trlf1  16312  trlres  16314