Definition df-f1o 5194

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 5186	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5184	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5185	. . 3 wff 𝐹:𝐴–onto→𝐵
7	5, 6	wa 103	. 2 wff (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵)
8	4, 7	wb 104	1 wff (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–1-1→𝐵 ∧ 𝐹:𝐴–onto→𝐵))

This definition is referenced by:  f1oeq1  5420  f1oeq2  5421  f1oeq3  5422  nff1o  5429  f1of1  5430  dff1o2  5436  dff1o5  5440  f1oco  5454  fo00  5467  dff1o6  5743  fcof1o  5756  tposf1o2  6234  cnref1o  9584  1arith  12293  reeff1o  13294  ioocosf1o  13375