Definition df-f1o 5340

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 5332	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5330	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5331	. . 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  5580  f1oeq2  5581  f1oeq3  5582  nff1o  5590  f1of1  5591  dff1o2  5597  dff1o5  5601  f1oco  5615  fo00  5630  dff1o6  5927  fcof1o  5940  tposf1o2  6479  cnref1o  9929  1arith  13003  xpsff1o  13495  znf1o  14730  reeff1o  15567  ioocosf1o  15648  mpodvdsmulf1o  15787  gausslemma2dlem1f1o  15862