Definition df-f1 3276

Description: Define a one-to-one function. For equivalent definitions see dff12 3771 and dff13 3988. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow).

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 3260	. 2 wff F:A-1-1->B
5	1, 2, 3	wf 3259	. . 3 wff F:A-->B
6	3	ccnv 3250	. . . 4 class `'F
7	6	wfun 3257	. . 3 wff Fun `'F
8	5, 7	wa 221	. 2 wff (F:A-->B /\ Fun `'F)
9	4, 8	wb 144	1 wff (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))

This definition is referenced by:  f1eq1 3767  f1eq2 3768  f1eq3 3769  hbf1 3770  dff12 3771  f1f 3772  f1cnv 3773  f1co 3774  dff1o2 3801  dff1o3 3802  f1f1orn 3807  f1ores 3811  f1imacnv 3813  f11o 3823  f10 3824  tz7.48lem 4256  abianfp 4263  ssdomg 4549  sbthlem9 4600  fodomr 4628  inf3lem7 4764  fodom 4944  reeff1o 7634  infxpidmlem7 7770  hmeogrp 11044  hartoglem 11435

Copyright terms: Public domain