MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fo Unicode version

Definition df-fo 5599
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 5804, dffo3 6046, dffo4 6047, and dffo5 6048. (Contributed by NM, 1-Aug-1994.)
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 5591 . 2
53, 1wfn 5588 . . 3
63crn 5005 . . . 4
76, 2wceq 1395 . . 3
85, 7wa 369 . 2
94, 8wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  foeq1  5796  foeq2  5797  foeq3  5798  nffo  5799  fof  5800  forn  5803  dffo2  5804  dffn4  5806  fores  5809  dff1o2  5826  dff1o3  5827  foimacnv  5838  foun  5839  fconst5  6128  fconstfvOLD  6134  dff1o6  6181  nvof1o  6186  f1oweALT  6784  fo1st  6820  fo2nd  6821  tposfo2  6997  fodomr  7688  f1finf1o  7766  unfilem2  7805  brwdom2  8020  harwdom  8037  infpwfien  8464  alephiso  8500  brdom3  8927  brdom5  8928  brdom4  8929  iunfo  8935  qnnen  13947  isfull2  15280  odf1o2  16593  cygctb  16894  qtopss  20216  qtopomap  20219  qtopcmap  20220  reeff1o  22842  efifo  22934  fargshiftfo  24638  pjfoi  26621  ghomfo  29031  bdayfo  29435  fobigcup  29550
  Copyright terms: Public domain W3C validator