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

Definition df-fn 5219
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 5211 . 2  wff  A  Fn  B
41wfun 5210 . . 3  wff  Fun  A
51cdm 4626 . . . 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  5246  fnsng  5263  fnprg  5271  fntpg  5272  fntp  5273  fncnv  5282  fneq1  5304  fneq2  5305  nffn  5312  fnfun  5313  fndm  5315  fnun  5322  fnco  5324  fnssresb  5328  fnres  5332  fnresi  5333  fn0  5335  fnopabg  5339  sbcfng  5363  fcoi1  5396  f00  5407  f1cnvcnv  5432  fores  5447  dff1o4  5469  foimacnv  5479  fun11iun  5482  funfvdm  5579  respreima  5644  fpr  5698  fnex  5738  fliftf  5799  fnoprabg  5975  tposfn2  6266  tfrlemibfn  6328  tfri1d  6335  tfr1onlembfn  6344  tfri1dALT  6351  tfrcllembfn  6357  sbthlemi9  6963  caseinl  7089  caseinr  7090  ctssdccl  7109  exmidfodomrlemim  7199  axaddf  7866  axmulf  7867  frecuzrdgtcl  10411  frecuzrdgtclt  10420  shftfn  10832  imasaddfnlemg  12734  fntopon  13494
  Copyright terms: Public domain W3C validator