Theorem funfn 5301

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 5274	. 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 4675   Fun wfun 5265   Fn wfn 5266

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 5274

This theorem is referenced by:  funfnd  5302  funssxp  5445  funforn  5505  funbrfvb  5621  funopfvb  5622  ssimaex  5640  fvco  5649  eqfunfv  5682  fvimacnvi  5694  unpreima  5705  respreima  5708  elrnrexdm  5719  elrnrexdmb  5720  ffvresb  5743  funiun  5761  funresdfunsnss  5787  resfunexg  5805  funex  5807  elunirn  5835  smores  6378  smores2  6380  tfrlem1  6394  funresdfunsndc  6592  fundmfibi  7040  resunimafz0  10976  fclim  11605