Theorem funfn 5347

Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)

Assertion

Ref	Expression
funfn	⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 2229	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 302	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5320	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 187	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1395  dom cdm 4718  Fun wfun 5311   Fn wfn 5312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1495  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-fn 5320

This theorem is referenced by:  funfnd  5348  funssxp  5492  funforn  5554  funbrfvb  5673  funopfvb  5674  ssimaex  5694  fvco  5703  eqfunfv  5736  fvimacnvi  5748  unpreima  5759  respreima  5762  elrnrexdm  5773  elrnrexdmb  5774  ffvresb  5797  funiun  5815  funresdfunsnss  5841  resfunexg  5859  funex  5861  elunirn  5889  smores  6436  smores2  6438  tfrlem1  6452  funresdfunsndc  6650  fundmfibi  7101  resunimafz0  11048  fclim  11800  ausgrumgrien  15962