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

Definition df-fn 4603
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5247, dffn3 5253, dffn4 5314, and dffn5 5420. (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 4587 . 2  wff  A  Fn  B
41wfun 4586 . . 3  wff  Fun  A
51cdm 4580 . . . 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  5141  fnsng  5156  fnprg  5162  fntp  5163  fncnv  5171  fneq1  5190  fneq2  5191  nffn  5197  fnfun  5198  fndm  5200  fnun  5207  fnco  5209  fnssresb  5213  fnres  5217  fnresi  5218  fn0  5220  fnopabg  5224  fcoi1  5272  f00  5283  f1cnvcnv  5302  fores  5317  dff1o4  5337  foimacnv  5347  fun11iun  5350  funfv  5438  fvimacnvALT  5496  respreima  5506  dff3  5525  fpr  5556  fnex  5593  fliftf  5666  f1oweALT  5703  fnoprabg  5797  curry1  6062  curry2  6065  tposfn2  6108  tfrlem10  6289  tfr1  6299  frfnom  6333  undifixp  6738  sbthlem9  6864  fodomr  6897  rankf  7350  cardf2  7460  axdc3lem2  7961  nqerf  8434  axaddf  8647  axmulf  8648  uzrdgfni  10899  hashkf  11217  shftfn  11445  imasaddfnlem  13304  imasvscafn  13313  cnrest  16845  ftc1cn  19222  grporn  20709  wfrlem13  23436  wfr1  23440  elno2  23475  bdayfn  23500  axdenselem1  23503  fnsingle  23632  fnimage  23642  imageval  23643  dfrdg4  23662  tfrqfree  23663  cmpdom  24309  repfuntw  24326  domrancur1b  24366  domrancur1c  24368  trnij  24781  cmpmor  25141  bnj145  27541  bnj1422  27656
  Copyright terms: Public domain W3C validator