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

Definition df-fo 5444
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 5641, dffo3 5874, dffo4 5875, and dffo5 5876. (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 5436 . 2
53, 1wfn 5433 . . 3
63crn 4863 . . . 4
76, 2wceq 1670 . . 3
85, 7wa 360 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  foeq1  5633  foeq2  5634  foeq3  5635  nffo  5636  fof  5637  forn  5640  dffo2  5641  dffn4  5643  fores  5646  dff1o2  5663  dff1o3  5664  foimacnv  5675  foun  5676  fconst5  5950  fconstfv  5955  dff1o6  5994  f1oweALT  6567  fo1st  6602  fo2nd  6603  tposfo2  6734  fodomr  7423  f1finf1o  7500  unfilem2  7538  brwdom2  7708  harwdom  7725  infpwfien  8114  alephiso  8150  brdom3  8577  brdom5  8578  brdom4  8579  iunfo  8585  qnnen  13343  isfull2  14662  odf1o2  15816  cygctb  16111  qtopss  18762  qtopomap  18765  qtopcmap  18766  reeff1o  21378  efifo  21469  fargshiftfo  22646  pjfoi  24228  nvof1o  25076  ghomfo  26450  bdayfo  26969  fobigcup  27084
  Copyright terms: Public domain W3C validator