Definition df-f1o 5384

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 5376	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5374	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5375	. . 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 used by:  f1oeq1  5627  f1oeq2  5628  f1oeq3  5629  nff1o  5637  f1of1  5638  dff1o2  5644  dff1o5  5648  f1oco  5662  fo00  5677  dff1o6  5982  fcof1o  5995  tposf1o2  6541  cnref1o  10051  1arith  13146  xpsff1o  13670  znf1o  14986  reeff1o  15874  ioocosf1o  15955  mpodvdsmulf1o  16104  gausslemma2dlem1f1o  16179