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

Definition df-fn 5238
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 5230 . 2  wff  A  Fn  B
41wfun 5229 . . 3  wff  Fun  A
51cdm 4644 . . . 4  class  dom  A
65, 2wceq 1364 . . 3  wff  dom  A  =  B
74, 6wa 104 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 105 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  5265  fnsng  5282  fnprg  5290  fntpg  5291  fntp  5292  fncnv  5301  fneq1  5323  fneq2  5324  nffn  5331  fnfun  5332  fndm  5334  fnun  5341  fnco  5343  fnssresb  5347  fnres  5351  fnresi  5352  fn0  5354  fnopabg  5358  sbcfng  5382  fcoi1  5415  f00  5426  f1cnvcnv  5451  fores  5466  dff1o4  5488  foimacnv  5498  fun11iun  5501  funfvdm  5600  respreima  5665  fpr  5719  fnex  5759  fliftf  5821  fnoprabg  5998  tposfn2  6292  tfrlemibfn  6354  tfri1d  6361  tfr1onlembfn  6370  tfri1dALT  6377  tfrcllembfn  6383  sbthlemi9  6995  caseinl  7121  caseinr  7122  ctssdccl  7141  exmidfodomrlemim  7231  axaddf  7898  axmulf  7899  frecuzrdgtcl  10445  frecuzrdgtclt  10454  shftfn  10868  imasaddfnlemg  12794  fntopon  14001
  Copyright terms: Public domain W3C validator