Definition df-f1 4792

Description: Define a one-to-one function. For equivalent definitions see dff12 5257 and dff13 5471. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by SF, 5-Jan-2015.)

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 4778	. 2 wff F:A-1-1->B
5	1, 2, 3	wf 4777	. . 3 wff F:A-->B
6	3	ccnv 4771	. . . 4 class `'F
7	6	wfun 4775	. . 3 wff Fun `'F
8	5, 7	wa 358	. 2 wff (F:A-->B /\ Fun `'F)
9	4, 8	wb 176	1 wff (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))

This definition is referenced by:  f1eq1  5253  f1eq2  5254  f1eq3  5255  nff1  5256  dff12  5257  f1f  5258  f1ss  5262  f1funfun  5263  f1co  5264  dff1o2  5291  f1f1orn  5297  f1ores  5300  f1imacnv  5302  fun11iun  5305  f11o  5315  f10  5316  enpw1  6062  ncdisjun  6136  sbthlem1  6203