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

Theorem funfn 5228
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 2170 . . 3  |-  dom  A  =  dom  A
21biantru 300 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 5201 . 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 1348   dom cdm 4611   Fun wfun 5192    Fn wfn 5193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-fn 5201
This theorem is referenced by:  funfnd  5229  funssxp  5367  funforn  5427  funbrfvb  5539  funopfvb  5540  ssimaex  5557  fvco  5566  eqfunfv  5598  fvimacnvi  5610  unpreima  5621  respreima  5624  elrnrexdm  5635  elrnrexdmb  5636  ffvresb  5659  funresdfunsnss  5699  resfunexg  5717  funex  5719  elunirn  5745  smores  6271  smores2  6273  tfrlem1  6287  funresdfunsndc  6485  fundmfibi  6916  resunimafz0  10766  fclim  11257
  Copyright terms: Public domain W3C validator