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

Definition df-fn 5215
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 5207 . 2  wff  A  Fn  B
41wfun 5206 . . 3  wff  Fun  A
51cdm 4623 . . . 4  class  dom  A
65, 2wceq 1353 . . 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  5242  fnsng  5259  fnprg  5267  fntpg  5268  fntp  5269  fncnv  5278  fneq1  5300  fneq2  5301  nffn  5308  fnfun  5309  fndm  5311  fnun  5318  fnco  5320  fnssresb  5324  fnres  5328  fnresi  5329  fn0  5331  fnopabg  5335  sbcfng  5359  fcoi1  5392  f00  5403  f1cnvcnv  5428  fores  5443  dff1o4  5465  foimacnv  5475  fun11iun  5478  funfvdm  5575  respreima  5640  fpr  5694  fnex  5734  fliftf  5794  fnoprabg  5970  tposfn2  6261  tfrlemibfn  6323  tfri1d  6330  tfr1onlembfn  6339  tfri1dALT  6346  tfrcllembfn  6352  sbthlemi9  6958  caseinl  7084  caseinr  7085  ctssdccl  7104  exmidfodomrlemim  7194  axaddf  7858  axmulf  7859  frecuzrdgtcl  10398  frecuzrdgtclt  10407  shftfn  10817  fntopon  13189
  Copyright terms: Public domain W3C validator