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

Definition df-fn 5492
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5627, dffn3 5633, dffn4 5694, and dffn5 5808. (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 5484 . 2  wff  A  Fn  B
41wfun 5483 . . 3  wff  Fun  A
51cdm 4913 . . . 4  class  dom  A
65, 2wceq 1654 . . 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  5517  fnsng  5533  fnprg  5540  fntpg  5541  fntp  5542  fncnv  5550  fneq1  5569  fneq2  5570  nffn  5576  fnfun  5577  fndm  5579  fnun  5586  fnco  5588  fnssresb  5592  fnres  5596  fnresi  5597  fn0  5599  fnopabg  5603  fcoi1  5652  f00  5663  f1cnvcnv  5682  fores  5697  dff1o4  5717  foimacnv  5727  fun11iun  5730  funfv  5826  fvimacnvALT  5885  respreima  5895  dff3  5918  fpr  5950  fnpr  5986  fnprOLD  5987  fnex  5997  fliftf  6073  f1oweALT  6110  fnoprabg  6207  curry1  6474  curry2  6477  tposfn2  6537  tfrlem10  6684  tfr1  6694  frfnom  6728  undifixp  7134  sbthlem9  7261  fodomr  7294  rankf  7756  cardf2  7868  axdc3lem2  8369  nqerf  8845  axaddf  9058  axmulf  9059  uzrdgfni  11336  hashkf  11658  shftfn  11926  imasaddfnlem  13791  imasvscafn  13800  cnrest  17387  cnextf  18135  ftc1cn  19965  grporn  21838  fdmrn  24074  mptfnf  24108  measdivcstOLD  24613  wfrlem13  25585  wfr1  25589  nofnbday  25642  elno2  25644  bdayfn  25669  fnsingle  25799  fnimage  25809  imageval  25810  dfrdg4  25830  tfrqfree  25831  ftc1cnnc  26321  fnresfnco  28078  funcoressn  28079  afvco2  28128  sbcfn  28188  bnj145  29268  bnj1422  29383
  Copyright terms: Public domain W3C validator