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

Definition df-fn 5084
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 5076 . 2  wff  A  Fn  B
41wfun 5075 . . 3  wff  Fun  A
51cdm 4499 . . . 4  class  dom  A
65, 2wceq 1314 . . 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  5111  fnsng  5128  fnprg  5136  fntpg  5137  fntp  5138  fncnv  5147  fneq1  5169  fneq2  5170  nffn  5177  fnfun  5178  fndm  5180  fnun  5187  fnco  5189  fnssresb  5193  fnres  5197  fnresi  5198  fn0  5200  fnopabg  5204  sbcfng  5228  fcoi1  5261  f00  5272  f1cnvcnv  5297  fores  5312  dff1o4  5331  foimacnv  5341  fun11iun  5344  funfvdm  5438  respreima  5502  fpr  5556  fnex  5596  fliftf  5654  fnoprabg  5826  tposfn2  6117  tfrlemibfn  6179  tfri1d  6186  tfr1onlembfn  6195  tfri1dALT  6202  tfrcllembfn  6208  sbthlemi9  6805  caseinl  6928  caseinr  6929  ctssdccl  6948  exmidfodomrlemim  7005  axaddf  7603  axmulf  7604  frecuzrdgtcl  10078  frecuzrdgtclt  10087  shftfn  10489  fntopon  12034
  Copyright terms: Public domain W3C validator