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

Definition df-fn 5416
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. For alternate definitions, see dffn2 5551, dffn3 5557, dffn4 5618, and dffn5 5731. (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 5408 . 2  wff  A  Fn  B
41wfun 5407 . . 3  wff  Fun  A
51cdm 4837 . . . 4  class  dom  A
65, 2wceq 1649 . . 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  5441  fnsng  5457  fnprg  5464  fntpg  5465  fntp  5466  fncnv  5474  fneq1  5493  fneq2  5494  nffn  5500  fnfun  5501  fndm  5503  fnun  5510  fnco  5512  fnssresb  5516  fnres  5520  fnresi  5521  fn0  5523  fnopabg  5527  fcoi1  5576  f00  5587  f1cnvcnv  5606  fores  5621  dff1o4  5641  foimacnv  5651  fun11iun  5654  funfv  5749  fvimacnvALT  5808  respreima  5818  dff3  5841  fpr  5873  fnpr  5909  fnprOLD  5910  fnex  5920  fliftf  5996  f1oweALT  6033  fnoprabg  6130  curry1  6397  curry2  6400  tposfn2  6460  tfrlem10  6607  tfr1  6617  frfnom  6651  undifixp  7057  sbthlem9  7184  fodomr  7217  rankf  7676  cardf2  7786  axdc3lem2  8287  nqerf  8763  axaddf  8976  axmulf  8977  uzrdgfni  11253  hashkf  11575  shftfn  11843  imasaddfnlem  13708  imasvscafn  13717  cnrest  17303  cnextf  18050  ftc1cn  19880  grporn  21753  fdmrn  23992  mptfnf  24026  measdivcstOLD  24531  wfrlem13  25482  wfr1  25486  nofnbday  25520  elno2  25522  bdayfn  25547  fnsingle  25672  fnimage  25682  imageval  25683  dfrdg4  25703  tfrqfree  25704  ftc1cnnc  26178  fnresfnco  27857  funcoressn  27858  afvco2  27907  bnj145  28800  bnj1422  28915
  Copyright terms: Public domain W3C validator