Definition df-f1 5264

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 5256	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5255	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4663	. . . 4 class ◡𝐹
7	6	wfun 5253	. . 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  5461  f1eq2  5462  f1eq3  5463  nff1  5464  dff12  5465  f1f  5466  f1ss  5472  f1ssr  5473  f1ssres  5475  f1cnvcnv  5477  f1co  5478  dff1o2  5512  f1f1orn  5518  f1imacnv  5524  fun11iun  5528  f11o  5540  f10  5541  f1o2ndf1  6295  ssdomg  6846  phplem4dom  6932  sbthlemi9  7040  casefun  7160  casef1  7165  djufun  7179  exmidfodomrlemim  7280  4sqlemffi  12590  ennnfonelemf1  12660