New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-fo GIF 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 (F:AontoB ↔ (F Fn A ran F = B))

Detailed syntax breakdown of Definition df-fo
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
3 cF . . 3 class F
41, 2, 3wfo 4779 . 2 wff F:AontoB
53, 1wfn 4776 . . 3 wff F Fn A
63crn 4773 . . . 4 class ran F
76, 2wceq 1642 . . 3 wff ran F = B
85, 7wa 358 . 2 wff (F Fn A ran F = B)
94, 8wb 176 1 wff (F:AontoB ↔ (F Fn A ran F = B))
 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