Theorem funfn 5289

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 2196	. . 3 |- dom A = dom A
2	1	biantru 302	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 5262	. 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 1364   dom cdm 4664   Fun wfun 5253   Fn wfn 5254

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 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-fn 5262

This theorem is referenced by:  funfnd  5290  funssxp  5428  funforn  5488  funbrfvb  5604  funopfvb  5605  ssimaex  5623  fvco  5632  eqfunfv  5665  fvimacnvi  5677  unpreima  5688  respreima  5691  elrnrexdm  5702  elrnrexdmb  5703  ffvresb  5726  funresdfunsnss  5766  resfunexg  5784  funex  5786  elunirn  5814  smores  6351  smores2  6353  tfrlem1  6367  funresdfunsndc  6565  fundmfibi  7005  resunimafz0  10925  fclim  11461