Definition df-f1o 5205

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 5197	. 2 wff 𝐹:𝐴–1-1-onto→𝐵
5	1, 2, 3	wf1 5195	. . 3 wff 𝐹:𝐴–1-1→𝐵
6	1, 2, 3	wfo 5196	. . 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  5431  f1oeq2  5432  f1oeq3  5433  nff1o  5440  f1of1  5441  dff1o2  5447  dff1o5  5451  f1oco  5465  fo00  5478  dff1o6  5755  fcof1o  5768  tposf1o2  6249  cnref1o  9609  1arith  12319  reeff1o  13488  ioocosf1o  13569