Definition df-f1 5233

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 5225	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5224	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4637	. . . 4 class ◡𝐹
7	6	wfun 5222	. . 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  5428  f1eq2  5429  f1eq3  5430  nff1  5431  dff12  5432  f1f  5433  f1ss  5439  f1ssr  5440  f1ssres  5442  f1cnvcnv  5444  f1co  5445  dff1o2  5478  f1f1orn  5484  f1imacnv  5490  fun11iun  5494  f11o  5506  f10  5507  f1o2ndf1  6243  ssdomg  6792  phplem4dom  6876  sbthlemi9  6978  casefun  7098  casef1  7103  djufun  7117  exmidfodomrlemim  7214  ennnfonelemf1  12433