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

Theorem funfn 5226
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 2170 . . 3 dom 𝐴 = dom 𝐴
21biantru 300 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 5199 . 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 1348  dom cdm 4609  Fun wfun 5190   Fn wfn 5191
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 1442  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-fn 5199
This theorem is referenced by:  funfnd  5227  funssxp  5365  funforn  5425  funbrfvb  5537  funopfvb  5538  ssimaex  5555  fvco  5564  eqfunfv  5596  fvimacnvi  5608  unpreima  5619  respreima  5622  elrnrexdm  5633  elrnrexdmb  5634  ffvresb  5657  funresdfunsnss  5697  resfunexg  5715  funex  5717  elunirn  5743  smores  6269  smores2  6271  tfrlem1  6285  funresdfunsndc  6483  fundmfibi  6913  resunimafz0  10755  fclim  11246
  Copyright terms: Public domain W3C validator