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

Definition df-fn 4670
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5314, dffn3 5320, dffn4 5381, and dffn5 5488. (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 4654 . 2  wff  A  Fn  B
41wfun 4653 . . 3  wff  Fun  A
51cdm 4647 . . . 4  class  dom  A
65, 2wceq 1619 . . 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  5208  fnsng  5223  fnprg  5229  fntp  5230  fncnv  5238  fneq1  5257  fneq2  5258  nffn  5264  fnfun  5265  fndm  5267  fnun  5274  fnco  5276  fnssresb  5280  fnres  5284  fnresi  5285  fn0  5287  fnopabg  5291  fcoi1  5339  f00  5350  f1cnvcnv  5369  fores  5384  dff1o4  5404  foimacnv  5414  fun11iun  5417  funfv  5506  fvimacnvALT  5564  respreima  5574  dff3  5593  fpr  5624  fnex  5661  fliftf  5734  f1oweALT  5771  fnoprabg  5865  curry1  6130  curry2  6133  tposfn2  6176  tfrlem10  6357  tfr1  6367  frfnom  6401  undifixp  6806  sbthlem9  6933  fodomr  6966  rankf  7420  cardf2  7530  axdc3lem2  8031  nqerf  8508  axaddf  8721  axmulf  8722  uzrdgfni  10973  hashkf  11291  shftfn  11519  imasaddfnlem  13378  imasvscafn  13387  cnrest  16961  ftc1cn  19338  grporn  20825  fdmrn  22982  wfrlem13  23623  wfr1  23627  elno2  23662  bdayfn  23687  axdenselem1  23690  fnsingle  23819  fnimage  23829  imageval  23830  dfrdg4  23849  tfrqfree  23850  cmpdom  24496  repfuntw  24513  domrancur1b  24553  domrancur1c  24555  trnij  24968  cmpmor  25328  bnj145  27788  bnj1422  27903
  Copyright terms: Public domain W3C validator