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

Definition df-fn 5393
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5530, dffn3 5536, dffn4 5596, and dffn5 5707. (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 5385 . 2
41wfun 5384 . . 3
51cdm 4811 . . . 4
65, 2wceq 1687 . . 3
74, 6wa 362 . 2
83, 7wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  funfn  5419  fnsng  5435  fnprg  5442  fntpg  5443  fntp  5444  fncnv  5452  fneq1  5469  fneq2  5470  nffn  5477  fnfun  5478  fndm  5480  fnun  5487  fnco  5489  fnssresb  5493  fnres  5497  fnresi  5498  fn0  5500  fnopabg  5504  sbcfng  5526  fdmrn  5543  fcoi1  5555  f00  5563  f1cnvcnv  5584  fores  5599  dff1o4  5619  foimacnv  5628  funfv  5728  fvimacnvALT  5792  respreima  5802  dff3  5826  fpr  5859  fnsnb  5867  fnprb  5905  fnprOLD  5906  fnex  5913  fliftf  5976  fnoprabg  6161  fun11iun  6506  f1oweALT  6530  curry1  6633  curry2  6636  tposfn2  6729  tfrlem10  6805  tfr1  6815  frfnom  6849  undifixp  7258  sbthlem9  7388  fodomr  7421  rankf  7948  cardf2  8060  axdc3lem2  8567  nqerf  9045  axaddf  9258  axmulf  9259  uzrdgfni  11722  hashkf  12046  shftfn  12503  imasaddfnlem  14406  imasvscafn  14415  cnrest  18593  cnextf  19342  ftc1cn  21215  grporn  23378  mptfnf  25656  ffsrn  25709  measdivcstOLD  26347  wfrlem13  27438  wfr1  27442  nofnbday  27495  elno2  27497  bdayfn  27522  fnsingle  27652  fnimage  27662  imageval  27663  dfrdg4  27683  tfrqfree  27684  ftc1cnnc  28137  fnresfnco  29706  funcoressn  29707  afvco2  29756  bnj145OLD  31296  bnj1422  31409
  Copyright terms: Public domain W3C validator