Theorem funfn 5302

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

Assertion

Ref	Expression
funfn	|- ( Fun A <-> A Fn dom A )

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 2205	. . 3 |- dom A = dom A
2	1	biantru 302	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 5275	. 2 |- ( A Fn dom A <-> ( Fun A /\ dom A = dom A ) )
4	2, 3	bitr4i 187	1 |- ( Fun A <-> A Fn dom A )

Syntax hints:   /\ wa 104   <-> wb 105   = wceq 1373   dom cdm 4676   Fun wfun 5266   Fn wfn 5267

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 1472  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-fn 5275

This theorem is referenced by:  funfnd  5303  funssxp  5447  funforn  5507  funbrfvb  5623  funopfvb  5624  ssimaex  5642  fvco  5651  eqfunfv  5684  fvimacnvi  5696  unpreima  5707  respreima  5710  elrnrexdm  5721  elrnrexdmb  5722  ffvresb  5745  funiun  5763  funresdfunsnss  5789  resfunexg  5807  funex  5809  elunirn  5837  smores  6380  smores2  6382  tfrlem1  6396  funresdfunsndc  6594  fundmfibi  7042  resunimafz0  10978  fclim  11638