Theorem funfn 5356

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 2231	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 302	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5329	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 187	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1397  dom cdm 4725  Fun wfun 5320   Fn wfn 5321

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 1497  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5329

This theorem is referenced by:  funfnd  5357  funssxp  5504  funforn  5566  funbrfvb  5686  funopfvb  5687  ssimaex  5707  fvco  5716  eqfunfv  5749  fvimacnvi  5761  unpreima  5772  respreima  5775  elrnrexdm  5786  elrnrexdmb  5787  ffvresb  5810  funiun  5829  funresdfunsnss  5857  resfunexg  5875  funex  5877  elunirn  5907  smores  6458  smores2  6460  tfrlem1  6474  funresdfunsndc  6674  fundmfibi  7137  resunimafz0  11096  fclim  11859  ausgrumgrien  16027