ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-fn Unicode version

Definition df-fn 4883
Description: Define a function with domain. Definition 6.15(1) of [TakeutiZaring] p. 27. (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 4875 . 2  wff  A  Fn  B
41wfun 4874 . . 3  wff  Fun  A
51cdm 4323 . . . 4  class  dom  A
65, 2wceq 1243 . . 3  wff  dom  A  =  B
74, 6wa 97 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 98 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  4909  fnsng  4925  fnprg  4932  fntpg  4933  fntp  4934  fncnv  4943  fneq1  4965  fneq2  4966  nffn  4973  fnfun  4974  fndm  4976  fnun  4983  fnco  4985  fnssresb  4989  fnres  4993  fnresi  4994  fn0  4996  fnopabg  5000  sbcfng  5022  fcoi1  5048  f00  5059  f1cnvcnv  5078  fores  5093  dff1o4  5112  foimacnv  5122  fun11iun  5125  funfvdm  5214  respreima  5273  fpr  5323  fnex  5361  fliftf  5417  fnoprabg  5580  tposfn2  5859  tfrlemibfn  5920  tfri1d  5927  frecuzrdgfn  9067  shftfn  9294
  Copyright terms: Public domain W3C validator