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

Definition df-fn 4932
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 4924 . 2  wff  A  Fn  B
41wfun 4923 . . 3  wff  Fun  A
51cdm 4372 . . . 4  class  dom  A
65, 2wceq 1259 . . 3  wff  dom  A  =  B
74, 6wa 101 . 2  wff  ( Fun 
A  /\  dom  A  =  B )
83, 7wb 102 1  wff  ( A  Fn  B  <->  ( Fun  A  /\  dom  A  =  B ) )
Colors of variables: wff set class
This definition is referenced by:  funfn  4958  fnsng  4974  fnprg  4981  fntpg  4982  fntp  4983  fncnv  4992  fneq1  5014  fneq2  5015  nffn  5022  fnfun  5023  fndm  5025  fnun  5032  fnco  5034  fnssresb  5038  fnres  5042  fnresi  5043  fn0  5045  fnopabg  5049  sbcfng  5071  fcoi1  5097  f00  5108  f1cnvcnv  5127  fores  5142  dff1o4  5161  foimacnv  5171  fun11iun  5174  funfvdm  5263  respreima  5322  fpr  5372  fnex  5410  fliftf  5466  fnoprabg  5629  tposfn2  5911  tfrlemibfn  5972  tfri1d  5979  frecuzrdgfn  9361  shftfn  9652
  Copyright terms: Public domain W3C validator