Definition df-f1 4931

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 4923	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 4922	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4364	. . . 4 class ◡𝐹
7	6	wfun 4920	. . 3 wff Fun ◡𝐹
8	5, 7	wa 102	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 103	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  5112  f1eq2  5113  f1eq3  5114  nff1  5115  dff12  5116  f1f  5117  f1ss  5122  f1ssr  5123  f1ssres  5124  f1cnvcnv  5125  f1co  5126  dff1o2  5156  f1f1orn  5162  f1imacnv  5168  fun11iun  5172  f11o  5184  f10  5185  f1o2ndf1  5874  ssdomg  6317  phplem4dom  6387