Definition df-f1o 5225

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 5217	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5215	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5216	. . 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  5451  f1oeq2  5452  f1oeq3  5453  nff1o  5461  f1of1  5462  dff1o2  5468  dff1o5  5472  f1oco  5486  fo00  5499  dff1o6  5780  fcof1o  5793  tposf1o2  6274  cnref1o  9653  1arith  12368  xpsff1o  12774  reeff1o  14334  ioocosf1o  14415