Theorem funfn 5354

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 5327	. 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 4723  Fun wfun 5318   Fn wfn 5319

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 5327

This theorem is referenced by:  funfnd  5355  funssxp  5501  funforn  5563  funbrfvb  5682  funopfvb  5683  ssimaex  5703  fvco  5712  eqfunfv  5745  fvimacnvi  5757  unpreima  5768  respreima  5771  elrnrexdm  5782  elrnrexdmb  5783  ffvresb  5806  funiun  5824  funresdfunsnss  5852  resfunexg  5870  funex  5872  elunirn  5902  smores  6453  smores2  6455  tfrlem1  6469  funresdfunsndc  6669  fundmfibi  7128  resunimafz0  11085  fclim  11845  ausgrumgrien  16009