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

Theorem funfn 4955
 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 2082 . . 3 dom 𝐴 = dom 𝐴
21biantru 296 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 4929 . 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 1285  dom cdm 4365  Fun wfun 4920   Fn wfn 4921 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 4929 This theorem is referenced by:  funssxp  5085  funforn  5138  funbrfvb  5242  funopfvb  5243  ssimaex  5260  fvco  5269  eqfunfv  5296  fvimacnvi  5307  unpreima  5318  respreima  5321  elrnrexdm  5332  elrnrexdmb  5333  ffvresb  5354  resfunexg  5408  funex  5410  elunirn  5431  smores  5935  smores2  5937  tfrlem1  5951  fundmfibi  6438  fclim  10260
 Copyright terms: Public domain W3C validator