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

Theorem funfn 5031
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 2088 . . 3 dom 𝐴 = dom 𝐴
21biantru 296 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 5005 . 2 (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
42, 3bitr4i 185 1 (Fun 𝐴𝐴 Fn dom 𝐴)
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103   = wceq 1289  dom cdm 4428  Fun wfun 4996   Fn wfn 4997
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 1383  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-fn 5005
This theorem is referenced by:  funssxp  5165  funforn  5224  funbrfvb  5331  funopfvb  5332  ssimaex  5349  fvco  5358  eqfunfv  5386  fvimacnvi  5397  unpreima  5408  respreima  5411  elrnrexdm  5422  elrnrexdmb  5423  ffvresb  5445  resfunexg  5500  funex  5502  elunirn  5527  smores  6039  smores2  6041  tfrlem1  6055  fundmfibi  6627  resunimafz0  10201  fclim  10646
  Copyright terms: Public domain W3C validator