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

Definition df-fn 4972
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 4964 . 2  wff  A  Fn  B
41wfun 4963 . . 3  wff  Fun  A
51cdm 4401 . . . 4  class  dom  A
65, 2wceq 1285 . . 3  wff  dom  A  =  B
74, 6wa 102 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 103 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  4998  fnsng  5014  fnprg  5022  fntpg  5023  fntp  5024  fncnv  5033  fneq1  5055  fneq2  5056  nffn  5063  fnfun  5064  fndm  5066  fnun  5073  fnco  5075  fnssresb  5079  fnres  5083  fnresi  5084  fn0  5086  fnopabg  5090  sbcfng  5112  fcoi1  5139  f00  5150  f1cnvcnv  5175  fores  5190  dff1o4  5209  foimacnv  5219  fun11iun  5222  funfvdm  5312  respreima  5372  fpr  5421  fnex  5459  fliftf  5518  fnoprabg  5681  tposfn2  5963  tfrlemibfn  6025  tfri1d  6032  tfr1onlembfn  6041  tfri1dALT  6048  tfrcllembfn  6054  exmidfodomrlemim  6730  frecuzrdgtcl  9708  frecuzrdgtclt  9717  shftfn  10086
  Copyright terms: Public domain W3C validator