Theorem funfn 5111

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 2115	. . 3 |- dom A = dom A
2	1	biantru 298	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 5084	. 2 |- ( A Fn dom A <-> ( Fun A /\ dom A = dom A ) )
4	2, 3	bitr4i 186	1 |- ( Fun A <-> A Fn dom A )

Syntax hints:   /\ wa 103   <-> wb 104   = wceq 1314   dom cdm 4499   Fun wfun 5075   Fn wfn 5076

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1408  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-fn 5084

This theorem is referenced by:  funfnd  5112  funssxp  5250  funforn  5310  funbrfvb  5418  funopfvb  5419  ssimaex  5436  fvco  5445  eqfunfv  5477  fvimacnvi  5488  unpreima  5499  respreima  5502  elrnrexdm  5513  elrnrexdmb  5514  ffvresb  5537  funresdfunsnss  5577  resfunexg  5595  funex  5597  elunirn  5621  smores  6143  smores2  6145  tfrlem1  6159  funresdfunsndc  6356  fundmfibi  6779  resunimafz0  10467  fclim  10955