Definition df-f1o 2437

Description: Define a one-to-one onto function. For equivalent definitions see f1o2 2804, f1o3 2805, f1o4 2807, and f1o5 2808. Compare Definition 6.15(6) of [TakeutiZaring] p. 27.

Assertion

Ref	Expression
df-f1o	⊢ (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))

Detailed syntax breakdown of Definition df-f1o

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf1o 2421	. 2 wff F:A–1-1-onto→B
5	1, 2, 3	wf1 2419	. . 3 wff F:A–1-1→B
6	1, 2, 3	wfo 2420	. . 3 wff F:A–onto→B
7	5, 6	wa 196	. 2 wff (F:A–1-1→B ∧ F:A–onto→B)
8	4, 7	wb 127	1 wff (F:A–1-1-onto→B ↔ (F:A–1-1→B ∧ F:A–onto→B))

This definition is referenced by:  f1oeq1 2795  f1oeq2 2796  f1oeq3 2797  hbf1o 2798  f1of1 2799  f1o2 2804  f1o3 2805  f1o5 2808  f1ococnv2 2817  f1oweOLD 2944  canth2 3381  ssfi 3430  unfilem2 3439  fiint 3445  alephiso 3697  ruc 4924

metamath.org