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

Definition df-fn 5274
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5406, dffn3 5412, dffn4 5473, and dffn5 5584. (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 5266 . 2  wff  A  Fn  B
41wfun 5265 . . 3  wff  Fun  A
51cdm 4705 . . . 4  class  dom  A
65, 2wceq 1632 . . 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  5299  fnsng  5315  fnprg  5321  fntp  5322  fncnv  5330  fneq1  5349  fneq2  5350  nffn  5356  fnfun  5357  fndm  5359  fnun  5366  fnco  5368  fnssresb  5372  fnres  5376  fnresi  5377  fn0  5379  fnopabg  5383  fcoi1  5431  f00  5442  f1cnvcnv  5461  fores  5476  dff1o4  5496  foimacnv  5506  fun11iun  5509  funfv  5602  fvimacnvALT  5660  respreima  5670  dff3  5689  fpr  5720  fnex  5757  fliftf  5830  f1oweALT  5867  fnoprabg  5961  curry1  6226  curry2  6229  tposfn2  6272  tfrlem10  6419  tfr1  6429  frfnom  6463  undifixp  6868  sbthlem9  6995  fodomr  7028  rankf  7482  cardf2  7592  axdc3lem2  8093  nqerf  8570  axaddf  8783  axmulf  8784  uzrdgfni  11037  hashkf  11355  shftfn  11584  imasaddfnlem  13446  imasvscafn  13455  cnrest  17029  ftc1cn  19406  grporn  20895  fdmrn  23051  mptfnf  23241  measdivcstOLD  23566  measdivcst  23567  wfrlem13  24339  wfr1  24343  nofnbday  24377  elno2  24379  bdayfn  24404  fnsingle  24529  fnimage  24539  imageval  24540  dfrdg4  24560  tfrqfree  24561  ftc1cnnc  25025  cmpdom  25246  repfuntw  25263  domrancur1b  25303  domrancur1c  25305  trnij  25718  cmpmor  26078  fnresfnco  28094  funcoressn  28095  afvco2  28144  bnj145  29071  bnj1422  29186
  Copyright terms: Public domain W3C validator