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  5828  funresdfunsnss  5856  resfunexg  5874  funex  5876  elunirn  5906  smores  6457  smores2  6459  tfrlem1  6473  funresdfunsndc  6673  fundmfibi  7136  resunimafz0  11094  fclim  11854  ausgrumgrien  16020