Definition df-f1 4793

Description: Define a one-to-one function. For equivalent definitions see dff12 5258 and dff13 5472. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by SF, 5-Jan-2015.)

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 4779	. 2 wff F:A–1-1→B
5	1, 2, 3	wf 4778	. . 3 wff F:A–→B
6	3	ccnv 4772	. . . 4 class ◡F
7	6	wfun 4776	. . 3 wff Fun ◡F
8	5, 7	wa 358	. 2 wff (F:A–→B ∧ Fun ◡F)
9	4, 8	wb 176	1 wff (F:A–1-1→B ↔ (F:A–→B ∧ Fun ◡F))

This definition is referenced by:  f1eq1  5254  f1eq2  5255  f1eq3  5256  nff1  5257  dff12  5258  f1f  5259  f1ss  5263  f1funfun  5264  f1co  5265  dff1o2  5292  f1f1orn  5298  f1ores  5301  f1imacnv  5303  fun11iun  5306  f11o  5316  f10  5317  enpw1  6063  ncdisjun  6137  sbthlem1  6204