Definition df-f1 3201

Description: Define a one-to-one function. For an equivalent definition see f11 3670. 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 3185	. 2 wff F:A-1-1->B
5	1, 2, 3	wf 3184	. . 3 wff F:A-->B
6	3	ccnv 3175	. . . 4 class `'F
7	6	wfun 3182	. . 3 wff Fun `'F
8	5, 7	wa 223	. 2 wff (F:A-->B /\ Fun `'F)
9	4, 8	wb 146	1 wff (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))

This definition is referenced by:  f1eq1 3666  f1eq2 3667  f1eq3 3668  hbf1 3669  f11 3670  f1f 3671  f1cnv 3672  f1co 3673  f1o2 3699  f1o3 3700  f1f1orn 3705  f1ores 3709  f1imacnv 3711  f11o 3718  f10 3719  tz7.48lem 3961  abianfp 3968  ssdomg 4414  sbthlem9 4461  fodomr 4489  inf3lem7 4628  fodom 4808  reeff1o 7426  infxpidmlem7 7559  hmeogrp 10524

Copyright terms: Public domain