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

Definition df-fn 5420
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5557, dffn3 5563, dffn4 5620, and dffn5 5730. (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 5412 . 2
41wfun 5411 . . 3
51cdm 4844 . . . 4
65, 2wceq 1662 . . 3
74, 6wa 360 . 2
83, 7wb 178 1
Colors of variables: wff set class
This definition is referenced by:  funfn  5446  fnsng  5462  fnprg  5469  fntpg  5470  fntp  5471  fncnv  5479  fneq1  5496  fneq2  5497  nffn  5504  fnfun  5505  fndm  5507  fnun  5514  fnco  5516  fnssresb  5520  fnres  5524  fnresi  5525  fn0  5527  fnopabg  5531  sbcfng  5553  fcoi1  5581  f00  5589  f1cnvcnv  5608  fores  5623  dff1o4  5643  foimacnv  5652  funfv  5751  fvimacnvALT  5811  respreima  5821  dff3  5844  fpr  5876  fnsnb  5884  fnprb  5915  fnprOLD  5916  fnex  5923  fliftf  5982  fnoprabg  6160  fun11iun  6499  f1oweALT  6522  curry1  6621  curry2  6624  tposfn2  6684  tfrlem10  6760  tfr1  6770  frfnom  6804  undifixp  7210  sbthlem9  7337  fodomr  7370  rankf  7832  cardf2  7944  axdc3lem2  8445  nqerf  8921  axaddf  9134  axmulf  9135  uzrdgfni  11573  hashkf  11897  shftfn  12348  imasaddfnlem  14244  imasvscafn  14253  cnrest  17852  cnextf  18601  ftc1cn  20431  grporn  22309  fdmrn  24565  mptfnf  24597  ffsrn  24650  measdivcstOLD  25309  wfrlem13  26380  wfr1  26384  nofnbday  26437  elno2  26439  bdayfn  26464  fnsingle  26594  fnimage  26604  imageval  26605  dfrdg4  26625  tfrqfree  26626  ftc1cnnc  27137  fnresfnco  28888  funcoressn  28889  afvco2  28938  bnj145OLD  30287  bnj1422  30402
  Copyright terms: Public domain W3C validator