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

Theorem funfn 5246
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 2177 . . 3  |-  dom  A  =  dom  A
21biantru 302 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5219 . 2  |-  ( A  Fn  dom  A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
42, 3bitr4i 187 1  |-  ( Fun 
A  <->  A  Fn  dom  A )
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105    = wceq 1353   dom cdm 4626   Fun wfun 5210    Fn wfn 5211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5219
This theorem is referenced by:  funfnd  5247  funssxp  5385  funforn  5445  funbrfvb  5558  funopfvb  5559  ssimaex  5577  fvco  5586  eqfunfv  5618  fvimacnvi  5630  unpreima  5641  respreima  5644  elrnrexdm  5655  elrnrexdmb  5656  ffvresb  5679  funresdfunsnss  5719  resfunexg  5737  funex  5739  elunirn  5766  smores  6292  smores2  6294  tfrlem1  6308  funresdfunsndc  6506  fundmfibi  6937  resunimafz0  10810  fclim  11301
  Copyright terms: Public domain W3C validator