Definition df-f1 5385

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

This definition is used by:  f1eq1  5596  f1eq2  5597  f1eq3  5598  nff1  5599  dff12  5600  f1f  5601  f1ss  5607  f1ssr  5608  f1ssres  5610  f1cnvcnv  5612  f1co  5613  dff1o2  5647  f1f1orn  5653  f1imacnv  5659  fun11iun  5663  f11o  5676  f10  5677  rinvf1o  6038  f1o2ndf1  6468  f1setexg  6956  ssdomg  7071  phplem4dom  7169  sbthlemi9  7289  casefun  7431  casef1  7436  djufun  7450  exmidfodomrlemim  7559  4sqlemffi  13203  ennnfonelemf1  13366  usgrislfuspgrdom  16653  subusgr  16738  trlf1  16851  trlres  16853