NFE Home 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
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3
41, 2, 3wf1o 4780 . 2
51, 2, 3wf1 4778 . . 3
61, 2, 3wfo 4779 . . 3
75, 6wa 358 . 2
84, 7wb 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
  Copyright terms: Public domain W3C validator