Theorem funfn 4951

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 2081	. . 3 |- dom A = dom A
2	1	biantru 296	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 4925	. 2 |- ( A Fn dom A <-> ( Fun A /\ dom A = dom A ) )
4	2, 3	bitr4i 185	1 |- ( Fun A <-> A Fn dom A )

Syntax hints:   /\ wa 102   <-> wb 103   = wceq 1284   dom cdm 4363   Fun wfun 4916   Fn wfn 4917

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-cleq 2074  df-fn 4925

This theorem is referenced by:  funssxp  5080  funforn  5133  funbrfvb  5237  funopfvb  5238  ssimaex  5255  fvco  5264  eqfunfv  5291  fvimacnvi  5302  unpreima  5313  respreima  5316  elrnrexdm  5327  elrnrexdmb  5328  ffvresb  5349  resfunexg  5403  funex  5405  elunirn  5426  smores  5930  smores2  5932  tfrlem1  5946  fundmfibi  6390  fclim  10133