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

Definition df-fn 5258
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5390, dffn3 5396, dffn4 5457, and dffn5 5568. (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 5250 . 2  wff  A  Fn  B
41wfun 5249 . . 3  wff  Fun  A
51cdm 4689 . . . 4  class  dom  A
65, 2wceq 1623 . . 3  wff  dom  A  =  B
74, 6wa 358 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 176 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  5283  fnsng  5299  fnprg  5305  fntp  5306  fncnv  5314  fneq1  5333  fneq2  5334  nffn  5340  fnfun  5341  fndm  5343  fnun  5350  fnco  5352  fnssresb  5356  fnres  5360  fnresi  5361  fn0  5363  fnopabg  5367  fcoi1  5415  f00  5426  f1cnvcnv  5445  fores  5460  dff1o4  5480  foimacnv  5490  fun11iun  5493  funfv  5586  fvimacnvALT  5644  respreima  5654  dff3  5673  fpr  5704  fnex  5741  fliftf  5814  f1oweALT  5851  fnoprabg  5945  curry1  6210  curry2  6213  tposfn2  6256  tfrlem10  6403  tfr1  6413  frfnom  6447  undifixp  6852  sbthlem9  6979  fodomr  7012  rankf  7466  cardf2  7576  axdc3lem2  8077  nqerf  8554  axaddf  8767  axmulf  8768  uzrdgfni  11021  hashkf  11339  shftfn  11568  imasaddfnlem  13430  imasvscafn  13439  cnrest  17013  ftc1cn  19390  grporn  20879  fdmrn  23035  mptfnf  23226  measdivcstOLD  23551  measdivcst  23552  wfrlem13  24268  wfr1  24272  nofnbday  24306  elno2  24308  bdayfn  24333  fnsingle  24458  fnimage  24468  imageval  24469  dfrdg4  24488  tfrqfree  24489  cmpdom  25143  repfuntw  25160  domrancur1b  25200  domrancur1c  25202  trnij  25615  cmpmor  25975  fnresfnco  27989  funcoressn  27990  afvco2  28037  bnj145  28755  bnj1422  28870
  Copyright terms: Public domain W3C validator