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

Theorem funfn 5247
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 5220 . 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 4627   Fun wfun 5211    Fn wfn 5212
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 5220
This theorem is referenced by:  funfnd  5248  funssxp  5386  funforn  5446  funbrfvb  5559  funopfvb  5560  ssimaex  5578  fvco  5587  eqfunfv  5619  fvimacnvi  5631  unpreima  5642  respreima  5645  elrnrexdm  5656  elrnrexdmb  5657  ffvresb  5680  funresdfunsnss  5720  resfunexg  5738  funex  5740  elunirn  5767  smores  6293  smores2  6295  tfrlem1  6309  funresdfunsndc  6507  fundmfibi  6938  resunimafz0  10811  fclim  11302
  Copyright terms: Public domain W3C validator