Definition df-f1o 4795

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5292, dff1o3 5293, dff1o4 5295, and dff1o5 5296. 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 SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-f1o	⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1o 4781	. 2 wff F:A–1-1-onto→B
5	1, 2, 3	wf1 4779	. . 3 wff F:A–1-1→B
6	1, 2, 3	wfo 4780	. . 3 wff F:A–onto→B
7	5, 6	wa 358	. 2 wff (F:A–1-1→B ∧ F:A–onto→B)
8	4, 7	wb 176	1 wff (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))

This definition is referenced by:  f1oeq1  5282  f1oeq2  5283  f1oeq3  5284  nff1o  5286  f1of1  5287  dff1o2  5292  dff1o5  5296  f1oco  5309  fo00  5319  f1o0  5320  dff1o6  5476