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

Theorem funfn 4931
 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 2040 . . 3 dom 𝐴 = dom 𝐴
21biantru 286 . 2 (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3 df-fn 4905 . 2 (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
42, 3bitr4i 176 1 (Fun 𝐴𝐴 Fn dom 𝐴)
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   = wceq 1243  dom cdm 4345  Fun wfun 4896   Fn wfn 4897 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-fn 4905 This theorem is referenced by:  funssxp  5060  funforn  5113  funbrfvb  5216  funopfvb  5217  ssimaex  5234  fvco  5243  eqfunfv  5270  fvimacnvi  5281  unpreima  5292  respreima  5295  elrnrexdm  5306  elrnrexdmb  5307  ffvresb  5328  resfunexg  5382  funex  5384  elunirn  5405  smores  5907  smores2  5909  tfrlem1  5923  fclim  9815
 Copyright terms: Public domain W3C validator