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

Definition df-fn 5540
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5680, dffn3 5686, dffn4 5748, and dffn5 5860. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fn

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wfn 5532 . 2
41wfun 5531 . . 3
51cdm 4957 . . . 4
65, 2wceq 1370 . . 3
74, 6wa 369 . 2
83, 7wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  funfn  5566  fnsng  5584  fnprg  5591  fntpg  5592  fntp  5593  fncnv  5601  fneq1  5618  fneq2  5619  nffn  5626  fnfun  5627  fndm  5629  fnun  5636  fnco  5638  fnssresb  5642  fnres  5646  fnresi  5647  fn0  5649  fnopabg  5653  sbcfng  5676  fdmrn  5694  fcoi1  5707  f00  5715  f1cnvcnv  5736  fores  5751  dff1o4  5771  foimacnv  5780  funfv  5881  fvimacnvALT  5945  respreima  5955  dff3  5979  fpr  6014  fnsnb  6022  fnprb  6061  fnprOLD  6062  fnex  6069  fliftf  6139  fnoprabg  6324  fun11iun  6670  f1oweALT  6694  curry1  6798  curry2  6801  tposfn2  6901  tfrlem10  6980  tfr1  6990  frfnom  7024  undifixp  7433  sbthlem9  7563  fodomr  7596  rankf  8138  cardf2  8250  axdc3lem2  8757  nqerf  9236  axaddf  9449  axmulf  9450  uzrdgfni  11926  hashkf  12262  shftfn  12720  imasaddfnlem  14625  imasvscafn  14634  cnrest  19288  cnextf  20037  ftc1cn  21915  grporn  24168  mptfnf  26443  ffsrn  26496  measdivcstOLD  27095  wfrlem13  28192  wfr1  28196  nofnbday  28249  elno2  28251  bdayfn  28276  fnsingle  28406  fnimage  28416  imageval  28417  dfrdg4  28437  tfrqfree  28438  ftc1cnnc  28926  fnresfnco  30909  funcoressn  30910  afvco2  30959  bnj145OLD  32561  bnj1422  32674
  Copyright terms: Public domain W3C validator