Definition df-f1 4907

Description: Define a one-to-one function. Compare Definition 6.15(5) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow). (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1	⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

Detailed syntax breakdown of Definition df-f1

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1 4899	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 4898	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4344	. . . 4 class ◡𝐹
7	6	wfun 4896	. . 3 wff Fun ◡𝐹
8	5, 7	wa 97	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 98	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  5087  f1eq2  5088  f1eq3  5089  nff1  5090  dff12  5091  f1f  5092  f1ss  5097  f1ssr  5098  f1ssres  5099  f1cnvcnv  5100  f1co  5101  dff1o2  5131  f1f1orn  5137  f1imacnv  5143  fun11iun  5147  f11o  5159  f10  5160  f1o2ndf1  5849  ssdomg  6258  phplem4dom  6324