Definition df-f1o 5331

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 5323	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5321	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5322	. . 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  5568  f1oeq2  5569  f1oeq3  5570  nff1o  5578  f1of1  5579  dff1o2  5585  dff1o5  5589  f1oco  5603  fo00  5617  dff1o6  5912  fcof1o  5925  tposf1o2  6431  cnref1o  9875  1arith  12930  xpsff1o  13422  znf1o  14655  reeff1o  15487  ioocosf1o  15568  mpodvdsmulf1o  15704  gausslemma2dlem1f1o  15779