Definition df-f1o 5359

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 5351	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5349	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5350	. . 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  5602  f1oeq2  5603  f1oeq3  5604  nff1o  5612  f1of1  5613  dff1o2  5619  dff1o5  5623  f1oco  5637  fo00  5652  dff1o6  5949  fcof1o  5962  tposf1o2  6501  cnref1o  9983  1arith  13065  xpsff1o  13562  znf1o  14799  reeff1o  15638  ioocosf1o  15719  mpodvdsmulf1o  15858  gausslemma2dlem1f1o  15933