Definition df-f1o 5195

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	|- ( 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 5187	. 2 wff F : A -1-1-onto-> B
5	1, 2, 3	wf1 5185	. . 3 wff F : A -1-1-> B
6	1, 2, 3	wfo 5186	. . 3 wff F : A -onto-> B
7	5, 6	wa 103	. 2 wff ( F : A -1-1-> B /\ F : A -onto-> B )
8	4, 7	wb 104	1 wff ( F : A -1-1-onto-> B <-> ( F : A -1-1-> B /\ F : A -onto-> B ) )

This definition is referenced by:  f1oeq1  5421  f1oeq2  5422  f1oeq3  5423  nff1o  5430  f1of1  5431  dff1o2  5437  dff1o5  5441  f1oco  5455  fo00  5468  dff1o6  5744  fcof1o  5757  tposf1o2  6238  cnref1o  9588  1arith  12297  reeff1o  13334  ioocosf1o  13415