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

Definition df-fn 5096
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 5088 . 2  wff  A  Fn  B
41wfun 5087 . . 3  wff  Fun  A
51cdm 4509 . . . 4  class  dom  A
65, 2wceq 1316 . . 3  wff  dom  A  =  B
74, 6wa 103 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 104 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  5123  fnsng  5140  fnprg  5148  fntpg  5149  fntp  5150  fncnv  5159  fneq1  5181  fneq2  5182  nffn  5189  fnfun  5190  fndm  5192  fnun  5199  fnco  5201  fnssresb  5205  fnres  5209  fnresi  5210  fn0  5212  fnopabg  5216  sbcfng  5240  fcoi1  5273  f00  5284  f1cnvcnv  5309  fores  5324  dff1o4  5343  foimacnv  5353  fun11iun  5356  funfvdm  5452  respreima  5516  fpr  5570  fnex  5610  fliftf  5668  fnoprabg  5840  tposfn2  6131  tfrlemibfn  6193  tfri1d  6200  tfr1onlembfn  6209  tfri1dALT  6216  tfrcllembfn  6222  sbthlemi9  6821  caseinl  6944  caseinr  6945  ctssdccl  6964  exmidfodomrlemim  7025  axaddf  7644  axmulf  7645  frecuzrdgtcl  10140  frecuzrdgtclt  10149  shftfn  10551  fntopon  12102
  Copyright terms: Public domain W3C validator