Theorem funfn 5161

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 2140	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 300	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5134	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 186	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1332  dom cdm 4547  Fun wfun 5125   Fn wfn 5126

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 1426  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-fn 5134

This theorem is referenced by:  funfnd  5162  funssxp  5300  funforn  5360  funbrfvb  5472  funopfvb  5473  ssimaex  5490  fvco  5499  eqfunfv  5531  fvimacnvi  5542  unpreima  5553  respreima  5556  elrnrexdm  5567  elrnrexdmb  5568  ffvresb  5591  funresdfunsnss  5631  resfunexg  5649  funex  5651  elunirn  5675  smores  6197  smores2  6199  tfrlem1  6213  funresdfunsndc  6410  fundmfibi  6835  resunimafz0  10606  fclim  11095