Definition df-f1 5221

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 5213	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5212	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4625	. . . 4 class ◡𝐹
7	6	wfun 5210	. . 3 wff Fun ◡𝐹
8	5, 7	wa 104	. 2 wff (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)
9	4, 8	wb 105	1 wff (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))

This definition is referenced by:  f1eq1  5416  f1eq2  5417  f1eq3  5418  nff1  5419  dff12  5420  f1f  5421  f1ss  5427  f1ssr  5428  f1ssres  5430  f1cnvcnv  5432  f1co  5433  dff1o2  5466  f1f1orn  5472  f1imacnv  5478  fun11iun  5482  f11o  5494  f10  5495  f1o2ndf1  6228  ssdomg  6777  phplem4dom  6861  sbthlemi9  6963  casefun  7083  casef1  7088  djufun  7102  exmidfodomrlemim  7199  ennnfonelemf1  12418