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

Definition df-fn 5504
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5639, dffn3 5645, dffn4 5706, and dffn5 5820. (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 5496 . 2
41wfun 5495 . . 3
51cdm 4919 . . . 4
65, 2wceq 1654 . . 3
74, 6wa 360 . 2
83, 7wb 178 1
Colors of variables: wff set class
This definition is referenced by:  funfn  5529  fnsng  5545  fnprg  5552  fntpg  5553  fntp  5554  fncnv  5562  fneq1  5581  fneq2  5582  nffn  5588  fnfun  5589  fndm  5591  fnun  5598  fnco  5600  fnssresb  5604  fnres  5608  fnresi  5609  fn0  5611  fnopabg  5615  fcoi1  5664  f00  5675  f1cnvcnv  5694  fores  5709  dff1o4  5729  foimacnv  5739  fun11iun  5742  funfv  5838  fvimacnvALT  5897  respreima  5907  dff3  5930  fpr  5962  fnpr  5998  fnprOLD  5999  fnex  6009  fliftf  6085  f1oweALT  6122  fnoprabg  6221  curry1  6488  curry2  6491  tposfn2  6551  tfrlem10  6697  tfr1  6707  frfnom  6741  undifixp  7147  sbthlem9  7274  fodomr  7307  rankf  7769  cardf2  7881  axdc3lem2  8382  nqerf  8858  axaddf  9071  axmulf  9072  uzrdgfni  11349  hashkf  11671  shftfn  11939  imasaddfnlem  13804  imasvscafn  13813  cnrest  17400  cnextf  18148  ftc1cn  19978  grporn  21851  fdmrn  24087  mptfnf  24121  measdivcstOLD  24627  ffsrn  24726  wfrlem13  25654  wfr1  25658  nofnbday  25711  elno2  25713  bdayfn  25738  fnsingle  25868  fnimage  25878  imageval  25879  dfrdg4  25899  tfrqfree  25900  ftc1cnnc  26390  fnresfnco  28145  funcoressn  28146  afvco2  28195  sbcfng  28254  bnj145  29335  bnj1422  29450
  Copyright terms: Public domain W3C validator