Definition df-f1 3185

Description: Define a one-to-one function. For an equivalent definition see f11 3649. 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 3169	. 2 wff F:A-1-1->B
5	1, 2, 3	wf 3168	. . 3 wff F:A-->B
6	3	ccnv 3159	. . . 4 class `'F
7	6	wfun 3166	. . 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 3645  f1eq2 3646  f1eq3 3647  hbf1 3648  f11 3649  f1f 3650  f1cnv 3651  f1co 3652  f1o2 3678  f1o3 3679  f1f1orn 3684  f1ores 3688  f1imacnv 3690  f11o 3697  f10 3698  tz7.48lem 3940  abianfp 3947  ssdomg 4389  sbthlem9 4435  fodomr 4463  inf3lem7 4591  fodom 4770  reeff1o 7368  infxpidmlem7 7501  hmeogrp 10425

Copyright terms: Public domain