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

Theorem funfn 4961
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 2082 . . 3  |-  dom  A  =  dom  A
21biantru 296 . 2  |-  ( Fun 
A  <->  ( Fun  A  /\  dom  A  =  dom  A ) )
3 df-fn 4935 . 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 1285   dom cdm 4371   Fun wfun 4926    Fn wfn 4927
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 1379  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-fn 4935
This theorem is referenced by:  funssxp  5091  funforn  5144  funbrfvb  5248  funopfvb  5249  ssimaex  5266  fvco  5275  eqfunfv  5302  fvimacnvi  5313  unpreima  5324  respreima  5327  elrnrexdm  5338  elrnrexdmb  5339  ffvresb  5360  resfunexg  5414  funex  5416  elunirn  5437  smores  5941  smores2  5943  tfrlem1  5957  fundmfibi  6448  fclim  10271
  Copyright terms: Public domain W3C validator