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

Theorem funfn 5153
 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 2139 . . 3 dom 𝐴 = dom 𝐴
21biantru 300 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 5126 . 2 (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
42, 3bitr4i 186 1 (Fun 𝐴𝐴 Fn dom 𝐴)
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1331  dom cdm 4539  Fun wfun 5117   Fn wfn 5118 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 1425  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-fn 5126 This theorem is referenced by:  funfnd  5154  funssxp  5292  funforn  5352  funbrfvb  5464  funopfvb  5465  ssimaex  5482  fvco  5491  eqfunfv  5523  fvimacnvi  5534  unpreima  5545  respreima  5548  elrnrexdm  5559  elrnrexdmb  5560  ffvresb  5583  funresdfunsnss  5623  resfunexg  5641  funex  5643  elunirn  5667  smores  6189  smores2  6191  tfrlem1  6205  funresdfunsndc  6402  fundmfibi  6827  resunimafz0  10586  fclim  11075
 Copyright terms: Public domain W3C validator