Definition df-f1o 5325

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 5317	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5315	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5316	. . 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  5562  f1oeq2  5563  f1oeq3  5564  nff1o  5572  f1of1  5573  dff1o2  5579  dff1o5  5583  f1oco  5597  fo00  5611  dff1o6  5906  fcof1o  5919  tposf1o2  6422  cnref1o  9858  1arith  12905  xpsff1o  13397  znf1o  14630  reeff1o  15462  ioocosf1o  15543  mpodvdsmulf1o  15679  gausslemma2dlem1f1o  15754