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

Theorem funfn 5045
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 2088 . . 3  |-  dom  A  =  dom  A
21biantru 296 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5018 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 185 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff set class
Syntax hints:    /\ wa 102    <-> wb 103    = wceq 1289   dom cdm 4438   Fun wfun 5009    Fn wfn 5010
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-fn 5018
This theorem is referenced by:  funssxp  5180  funforn  5240  funbrfvb  5347  funopfvb  5348  ssimaex  5365  fvco  5374  eqfunfv  5402  fvimacnvi  5413  unpreima  5424  respreima  5427  elrnrexdm  5438  elrnrexdmb  5439  ffvresb  5461  funresdfunsnss  5500  resfunexg  5518  funex  5520  elunirn  5545  smores  6057  smores2  6059  tfrlem1  6073  fundmfibi  6646  resunimafz0  10232  fclim  10678
  Copyright terms: Public domain W3C validator