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

Definition df-fn 5397
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5532, dffn3 5538, dffn4 5599, and dffn5 5711. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-fn  |-  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )

Detailed syntax breakdown of Definition df-fn
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wfn 5389 . 2  wff  A  Fn  B
41wfun 5388 . . 3  wff  Fun  A
51cdm 4818 . . . 4  class  dom  A
65, 2wceq 1649 . . 3  wff  dom  A  =  B
74, 6wa 359 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 177 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  5422  fnsng  5438  fnprg  5445  fntpg  5446  fntp  5447  fncnv  5455  fneq1  5474  fneq2  5475  nffn  5481  fnfun  5482  fndm  5484  fnun  5491  fnco  5493  fnssresb  5497  fnres  5501  fnresi  5502  fn0  5504  fnopabg  5508  fcoi1  5557  f00  5568  f1cnvcnv  5587  fores  5602  dff1o4  5622  foimacnv  5632  fun11iun  5635  funfv  5729  fvimacnvALT  5788  respreima  5798  dff3  5821  fpr  5853  fnpr  5889  fnprOLD  5890  fnex  5900  fliftf  5976  f1oweALT  6013  fnoprabg  6110  curry1  6377  curry2  6380  tposfn2  6437  tfrlem10  6584  tfr1  6594  frfnom  6628  undifixp  7034  sbthlem9  7161  fodomr  7194  rankf  7653  cardf2  7763  axdc3lem2  8264  nqerf  8740  axaddf  8953  axmulf  8954  uzrdgfni  11225  hashkf  11547  shftfn  11815  imasaddfnlem  13680  imasvscafn  13689  cnrest  17271  cnextf  18018  ftc1cn  19794  grporn  21648  fdmrn  23882  mptfnf  23915  measdivcstOLD  24372  wfrlem13  25292  wfr1  25296  nofnbday  25330  elno2  25332  bdayfn  25357  fnsingle  25482  fnimage  25492  imageval  25493  dfrdg4  25513  tfrqfree  25514  ftc1cnnc  25979  fnresfnco  27659  funcoressn  27660  afvco2  27709  bnj145  28432  bnj1422  28547
  Copyright terms: Public domain W3C validator