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

Definition df-fo 4793
Description: Define an onto function. Definition 6.15(4) of [TakeutiZaring] p. 27. We use their notation ("onto" under the arrow). For alternate definitions, see dffo2 5273, dffo3 5422, dffo4 5423, and dffo5 5424. (Contributed by SF, 5-Jan-2015.)
Assertion
Ref Expression
df-fo

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cF . . 3
41, 2, 3wfo 4779 . 2
53, 1wfn 4776 . . 3
63crn 4773 . . . 4
76, 2wceq 1642 . . 3
85, 7wa 358 . 2
94, 8wb 176 1
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  5265  foeq2  5266  foeq3  5267  nffo  5268  fof  5269  forn  5272  dffo2  5273  dffn4  5275  fores  5278  dff1o2  5291  dff1o3  5292  foimacnv  5303  f1o0  5319  fconst5  5455  fconstfv  5456  dff1o6  5475  1stfo  5505  2ndfo  5506
  Copyright terms: Public domain W3C validator