Definition df-f1 5285

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 5277	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5276	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4682	. . . 4 class ◡𝐹
7	6	wfun 5274	. . 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  5488  f1eq2  5489  f1eq3  5490  nff1  5491  dff12  5492  f1f  5493  f1ss  5499  f1ssr  5500  f1ssres  5502  f1cnvcnv  5504  f1co  5505  dff1o2  5539  f1f1orn  5545  f1imacnv  5551  fun11iun  5555  f11o  5567  f10  5568  f1o2ndf1  6327  ssdomg  6883  phplem4dom  6974  sbthlemi9  7082  casefun  7202  casef1  7207  djufun  7221  exmidfodomrlemim  7325  4sqlemffi  12794  ennnfonelemf1  12864