Definition df-f1 2435

Description: Define a one-to-one function. For an equivalent definition see f11 2780. Compare Definition 6.15(5) of [TakeutiZaring] p. 27.

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 2419	. 2 wff F:A–1-1→B
5	1, 2, 3	wf 2418	. . 3 wff F:A–→B
6	3	ccnv 2409	. . . 4 class ◡F
7	6	wfun 2416	. . 3 wff Fun ◡F
8	5, 7	wa 196	. 2 wff (F:A–→B ∧ Fun ◡F)
9	4, 8	wb 127	1 wff (F:A–1-1→B ↔ (F:A–→B ∧ Fun ◡F))

This definition is referenced by:  f1eq1 2776  f1eq2 2777  f1eq3 2778  hbf1 2779  f11 2780  f1f 2781  f1cnv 2782  f1co 2783  f1o2 2804  f1o3 2805  f1f1orn 2810  f1ores 2813  f1imacnv 2814  f11o 2821  f10 2822  tz7.48lem 2993  abianfp 3000  ssdomg 3311  sbthlem9 3357  inf3lem7 3470  fodom 3613  fodomb 3615  infxpidmlem7 4939

metamath.org