Definition df-f1o 5138

Description: Define a one-to-one onto function. Compare Definition 6.15(6) of [TakeutiZaring] p. 27. We use their notation ("1-1" above the arrow and "onto" below the arrow). (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f1o	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf1o 5130	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5128	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5129	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 103	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 104	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  5364  f1oeq2  5365  f1oeq3  5366  nff1o  5373  f1of1  5374  dff1o2  5380  dff1o5  5384  f1oco  5398  fo00  5411  dff1o6  5685  fcof1o  5698  tposf1o2  6175  cnref1o  9469  reeff1o  12902  ioocosf1o  12983