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

Definition df-fo 5507
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 5704, dffo3 5932, dffo4 5933, and dffo5 5934. (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 5499 . 2
53, 1wfn 5496 . . 3
63crn 4920 . . . 4
76, 2wceq 1654 . . 3
85, 7wa 360 . 2
94, 8wb 178 1
Colors of variables: wff set class
This definition is referenced by:  foeq1  5696  foeq2  5697  foeq3  5698  nffo  5699  fof  5700  forn  5703  dffo2  5704  dffn4  5706  fores  5709  dff1o2  5726  dff1o3  5727  foimacnv  5739  foun  5740  fconst5  5997  fconstfv  6002  dff1o6  6061  f1oweALT  6122  fo1st  6416  fo2nd  6417  tposfo2  6552  fodomr  7307  f1finf1o  7384  unfilem2  7421  brwdom2  7590  harwdom  7607  infpwfien  7994  alephiso  8030  brdom3  8457  brdom5  8458  brdom4  8459  iunfo  8465  qnnen  12864  isfull2  14159  odf1o2  15258  cygctb  15552  qtopss  17798  qtopomap  17801  qtopcmap  17802  reeff1o  20414  efifo  20500  fargshiftfo  21676  pjfoi  23256  nvof1o  24088  ghomfo  25206  bdayfo  25734  fobigcup  25849
  Copyright terms: Public domain W3C validator