Definition df-f1o 5262

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 5254	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5252	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5253	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 104	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 105	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  5489  f1oeq2  5490  f1oeq3  5491  nff1o  5499  f1of1  5500  dff1o2  5506  dff1o5  5510  f1oco  5524  fo00  5537  dff1o6  5820  fcof1o  5833  tposf1o2  6325  cnref1o  9719  1arith  12508  xpsff1o  12935  znf1o  14150  reeff1o  14949  ioocosf1o  15030  gausslemma2dlem1f1o  15217