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

Theorem funfn 4956
Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)
Assertion
Ref Expression
funfn (Fun 𝐴𝐴 Fn dom 𝐴)

Proof of Theorem funfn
StepHypRef Expression
1 eqid 2054 . . 3 dom 𝐴 = dom 𝐴
21biantru 290 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 4930 . 2 (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
42, 3bitr4i 180 1 (Fun 𝐴𝐴 Fn dom 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102   = wceq 1257  dom cdm 4370  Fun wfun 4921   Fn wfn 4922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1352  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-cleq 2047  df-fn 4930
This theorem is referenced by:  funssxp  5085  funforn  5138  funbrfvb  5241  funopfvb  5242  ssimaex  5259  fvco  5268  eqfunfv  5295  fvimacnvi  5306  unpreima  5317  respreima  5320  elrnrexdm  5331  elrnrexdmb  5332  ffvresb  5353  resfunexg  5407  funex  5409  elunirn  5430  smores  5935  smores2  5937  tfrlem1  5951  fclim  10009
  Copyright terms: Public domain W3C validator