Definition df-f1 4176

Description: Define a one-to-one function. For equivalent definitions see dff12 4735 and dff13 4984. 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 4160	. 2 wff F:A-1-1->B
5	1, 2, 3	wf 4159	. . 3 wff F:A-->B
6	3	ccnv 4150	. . . 4 class `'F
7	6	wfun 4157	. . 3 wff Fun `'F
8	5, 7	wa 433	. 2 wff (F:A-->B /\ Fun `'F)
9	4, 8	wb 231	1 wff (F:A-1-1->B <-> (F:A-->B /\ Fun `'F))

This definition is referenced by:  f1eq1 4731  f1eq2 4732  f1eq3 4733  hbf1 4734  dff12 4735  f1f 4736  f1ss 4737  f1cnvcnv 4738  f1co 4739  dff1o2 4766  f1f1orn 4772  f1ores 4776  f1imacnv 4778  f11o 4791  f10 4792  tz7.48lem 5368  abianfp 5378  ssdomg 5671  sbthlem9 5727  fodomr 5759  1sdom 5859  inf3lem7OLD 6002  fodomnumlem 6273  fodom 6448  reeff1o 9207  infxpidmlem7OLD 9357  injrec2 15439  hmeogrp 15910  hartoglem 16468

Copyright terms: Public domain