Definition df-f1o 5379

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 5371	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5369	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5370	. . 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  5622  f1oeq2  5623  f1oeq3  5624  nff1o  5632  f1of1  5633  dff1o2  5639  dff1o5  5643  f1oco  5657  fo00  5672  dff1o6  5972  fcof1o  5985  tposf1o2  6531  cnref1o  10030  1arith  13124  xpsff1o  13647  znf1o  14958  reeff1o  15797  ioocosf1o  15878  mpodvdsmulf1o  16018  gausslemma2dlem1f1o  16093