Theorem funfn 5288

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 5261	. 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 4663   Fun wfun 5252   Fn wfn 5253

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 5261

This theorem is referenced by:  funfnd  5289  funssxp  5427  funforn  5487  funbrfvb  5603  funopfvb  5604  ssimaex  5622  fvco  5631  eqfunfv  5664  fvimacnvi  5676  unpreima  5687  respreima  5690  elrnrexdm  5701  elrnrexdmb  5702  ffvresb  5725  funresdfunsnss  5765  resfunexg  5783  funex  5785  elunirn  5813  smores  6350  smores2  6352  tfrlem1  6366  funresdfunsndc  6564  fundmfibi  7004  resunimafz0  10923  fclim  11459