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

Definition df-fn 4984
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 4976 . 2  wff  A  Fn  B
41wfun 4975 . . 3  wff  Fun  A
51cdm 4411 . . . 4  class  dom  A
65, 2wceq 1287 . . 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  5010  fnsng  5026  fnprg  5034  fntpg  5035  fntp  5036  fncnv  5045  fneq1  5067  fneq2  5068  nffn  5075  fnfun  5076  fndm  5078  fnun  5085  fnco  5087  fnssresb  5091  fnres  5095  fnresi  5096  fn0  5098  fnopabg  5102  sbcfng  5124  fcoi1  5154  f00  5165  f1cnvcnv  5190  fores  5205  dff1o4  5224  foimacnv  5234  fun11iun  5237  funfvdm  5330  respreima  5390  fpr  5442  fnex  5480  fliftf  5539  fnoprabg  5703  tposfn2  5985  tfrlemibfn  6047  tfri1d  6054  tfr1onlembfn  6063  tfri1dALT  6070  tfrcllembfn  6076  sbthlemi9  6618  exmidfodomrlemim  6771  frecuzrdgtcl  9747  frecuzrdgtclt  9756  shftfn  10155
  Copyright terms: Public domain W3C validator