Definition df-f1 5260

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 5252	. 2 wff 𝐹:𝐴–1-1→𝐵
5	1, 2, 3	wf 5251	. . 3 wff 𝐹:𝐴⟶𝐵
6	3	ccnv 4659	. . . 4 class ◡𝐹
7	6	wfun 5249	. . 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  5455  f1eq2  5456  f1eq3  5457  nff1  5458  dff12  5459  f1f  5460  f1ss  5466  f1ssr  5467  f1ssres  5469  f1cnvcnv  5471  f1co  5472  dff1o2  5506  f1f1orn  5512  f1imacnv  5518  fun11iun  5522  f11o  5534  f10  5535  f1o2ndf1  6283  ssdomg  6834  phplem4dom  6920  sbthlemi9  7026  casefun  7146  casef1  7151  djufun  7165  exmidfodomrlemim  7263  4sqlemffi  12537  ennnfonelemf1  12578