Definition df-f1o 5324

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 5316	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5314	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5315	. . 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  5559  f1oeq2  5560  f1oeq3  5561  nff1o  5569  f1of1  5570  dff1o2  5576  dff1o5  5580  f1oco  5594  fo00  5608  dff1o6  5899  fcof1o  5912  tposf1o2  6414  cnref1o  9842  1arith  12885  xpsff1o  13377  znf1o  14609  reeff1o  15441  ioocosf1o  15522  mpodvdsmulf1o  15658  gausslemma2dlem1f1o  15733