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

Definition df-fn 5449
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5584, dffn3 5590, dffn4 5651, and dffn5 5764. (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 5441 . 2  wff  A  Fn  B
41wfun 5440 . . 3  wff  Fun  A
51cdm 4870 . . . 4  class  dom  A
65, 2wceq 1652 . . 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  5474  fnsng  5490  fnprg  5497  fntpg  5498  fntp  5499  fncnv  5507  fneq1  5526  fneq2  5527  nffn  5533  fnfun  5534  fndm  5536  fnun  5543  fnco  5545  fnssresb  5549  fnres  5553  fnresi  5554  fn0  5556  fnopabg  5560  fcoi1  5609  f00  5620  f1cnvcnv  5639  fores  5654  dff1o4  5674  foimacnv  5684  fun11iun  5687  funfv  5782  fvimacnvALT  5841  respreima  5851  dff3  5874  fpr  5906  fnpr  5942  fnprOLD  5943  fnex  5953  fliftf  6029  f1oweALT  6066  fnoprabg  6163  curry1  6430  curry2  6433  tposfn2  6493  tfrlem10  6640  tfr1  6650  frfnom  6684  undifixp  7090  sbthlem9  7217  fodomr  7250  rankf  7712  cardf2  7822  axdc3lem2  8323  nqerf  8799  axaddf  9012  axmulf  9013  uzrdgfni  11290  hashkf  11612  shftfn  11880  imasaddfnlem  13745  imasvscafn  13754  cnrest  17341  cnextf  18089  ftc1cn  19919  grporn  21792  fdmrn  24031  mptfnf  24065  measdivcstOLD  24570  wfrlem13  25542  wfr1  25546  nofnbday  25599  elno2  25601  bdayfn  25626  fnsingle  25756  fnimage  25766  imageval  25767  dfrdg4  25787  tfrqfree  25788  ftc1cnnc  26269  fnresfnco  27957  funcoressn  27958  afvco2  28007  bnj145  29031  bnj1422  29146
  Copyright terms: Public domain W3C validator