df-f1o - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > df-f1o		Unicode version

Definition df-f1o 4794

Description: Define a one-to-one onto function. For equivalent definitions see dff1o2 5291, dff1o3 5292, dff1o4 5294, and dff1o5 5295. 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 SF, 5-Jan-2015.)

**Assertion**
Ref	Expression
df-f1o	$/\$

**Detailed syntax breakdown of Definition df-f1o**
Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3		cF	. . 3
4	1, 2, 3	wf1o 4780	. 2
5	1, 2, 3	wf1 4778	. . 3
6	1, 2, 3	wfo 4779	. . 3
7	5, 6	wa 358	. 2 $/\$
8	4, 7	wb 176	1 $/\$

Colors of variables: wff setvar class

This definition is referenced by: f1oeq1 5281 f1oeq2 5282 f1oeq3 5283 nff1o 5285 f1of1 5286 dff1o2 5291 dff1o5 5295 f1oco 5308 fo00 5318 f1o0 5319 dff1o6 5475

W3C validator