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 5555, dffn3 5561, dffn4 5622, and dffn5 5735. (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 5412 . 2  wff  A  Fn  B
41wfun 5411 . . 3  wff  Fun  A
51cdm 4841 . . . 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  5445  fnsng  5461  fnprg  5468  fntpg  5469  fntp  5470  fncnv  5478  fneq1  5497  fneq2  5498  nffn  5504  fnfun  5505  fndm  5507  fnun  5514  fnco  5516  fnssresb  5520  fnres  5524  fnresi  5525  fn0  5527  fnopabg  5531  fcoi1  5580  f00  5591  f1cnvcnv  5610  fores  5625  dff1o4  5645  foimacnv  5655  fun11iun  5658  funfv  5753  fvimacnvALT  5812  respreima  5822  dff3  5845  fpr  5877  fnpr  5913  fnprOLD  5914  fnex  5924  fliftf  6000  f1oweALT  6037  fnoprabg  6134  curry1  6401  curry2  6404  tposfn2  6464  tfrlem10  6611  tfr1  6621  frfnom  6655  undifixp  7061  sbthlem9  7188  fodomr  7221  rankf  7680  cardf2  7790  axdc3lem2  8291  nqerf  8767  axaddf  8980  axmulf  8981  uzrdgfni  11257  hashkf  11579  shftfn  11847  imasaddfnlem  13712  imasvscafn  13721  cnrest  17307  cnextf  18054  ftc1cn  19884  grporn  21757  fdmrn  23996  mptfnf  24030  measdivcstOLD  24535  wfrlem13  25486  wfr1  25490  nofnbday  25524  elno2  25526  bdayfn  25551  fnsingle  25676  fnimage  25686  imageval  25687  dfrdg4  25707  tfrqfree  25708  ftc1cnnc  26182  fnresfnco  27861  funcoressn  27862  afvco2  27911  bnj145  28804  bnj1422  28919
  Copyright terms: Public domain W3C validator