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

Theorem funfn 5111
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
Assertion
Ref Expression
funfn  |-  ( Fun 
A  <->  A  Fn  dom  A )

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2115 . . 3  |-  dom  A  =  dom  A
21biantru 298 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5084 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 186 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104    = wceq 1314   dom cdm 4499   Fun wfun 5075    Fn wfn 5076
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-fn 5084
This theorem is referenced by:  funfnd  5112  funssxp  5250  funforn  5310  funbrfvb  5418  funopfvb  5419  ssimaex  5436  fvco  5445  eqfunfv  5477  fvimacnvi  5488  unpreima  5499  respreima  5502  elrnrexdm  5513  elrnrexdmb  5514  ffvresb  5537  funresdfunsnss  5577  resfunexg  5595  funex  5597  elunirn  5621  smores  6143  smores2  6145  tfrlem1  6159  funresdfunsndc  6356  fundmfibi  6779  resunimafz0  10467  fclim  10955
  Copyright terms: Public domain W3C validator