Definition df-f1 4011

Description: Define a one-to-one function. For equivalent definitions see dff12 4609 and dff13 4850. 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 3995	. 2 wff F:A-1-1->B
5	1, 2, 3	wf 3994	. . 3 wff F:A-->B
6	3	ccnv 3985	. . . 4 class `'F
7	6	wfun 3992	. . 3 wff Fun `'F
8	5, 7	wa 240	. 2 wff (F:A-->B /\ Fun `'F)
9	4, 8	wb 163	1 wff (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))

This definition is referenced by:  f1eq1 4605  f1eq2 4606  f1eq3 4607  hbf1 4608  dff12 4609  f1f 4610  f1cnv 4611  f1co 4612  dff1o2 4639  dff1o2OLD 4640  dff1o3OLD 4642  f1f1orn 4649  f1ores 4654  f1imacnv 4656  f11o 4666  f10 4667  tz7.48lem 5164  abianfp 5171  ssdomg 5467  sbthlem9 5518  fodomr 5547  hartoglem 5692  inf3lem7 5725  fodom 5960  reeff1o 8691  infxpidmlem7 8827  injrec2 14466  hmeogrp 14892  hartoglemOLD 15383

Copyright terms: Public domain