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

Definition df-fn 5226
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5357, dffn3 5363, dffn4 5424, and dffn5 5531. (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 5218 . 2  wff  A  Fn  B
41wfun 5217 . . 3  wff  Fun  A
51cdm 4690 . . . 4  class  dom  A
65, 2wceq 1625 . . 3  wff  dom  A  =  B
74, 6wa 360 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 178 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  5251  fnsng  5266  fnprg  5272  fntp  5273  fncnv  5281  fneq1  5300  fneq2  5301  nffn  5307  fnfun  5308  fndm  5310  fnun  5317  fnco  5319  fnssresb  5323  fnres  5327  fnresi  5328  fn0  5330  fnopabg  5334  fcoi1  5382  f00  5393  f1cnvcnv  5412  fores  5427  dff1o4  5447  foimacnv  5457  fun11iun  5460  funfv  5549  fvimacnvALT  5607  respreima  5617  dff3  5636  fpr  5667  fnex  5704  fliftf  5777  f1oweALT  5814  fnoprabg  5908  curry1  6173  curry2  6176  tposfn2  6219  tfrlem10  6400  tfr1  6410  frfnom  6444  undifixp  6849  sbthlem9  6976  fodomr  7009  rankf  7463  cardf2  7573  axdc3lem2  8074  nqerf  8551  axaddf  8764  axmulf  8765  uzrdgfni  11017  hashkf  11335  shftfn  11564  imasaddfnlem  13426  imasvscafn  13435  cnrest  17009  ftc1cn  19386  grporn  20873  fdmrn  23030  wfrlem13  23671  wfr1  23675  elno2  23710  bdayfn  23735  axdenselem1  23738  fnsingle  23867  fnimage  23877  imageval  23878  dfrdg4  23897  tfrqfree  23898  cmpdom  24544  repfuntw  24561  domrancur1b  24601  domrancur1c  24603  trnij  25016  cmpmor  25376  fnresfnco  27370  funcoressn  27371  afvco2  27418  bnj145  28024  bnj1422  28139
  Copyright terms: Public domain W3C validator