Theorem funfn 5045

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 2088	. . 3 |- dom A = dom A
2	1	biantru 296	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 5018	. 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 1289   dom cdm 4438   Fun wfun 5009   Fn wfn 5010

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 1383  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-fn 5018

This theorem is referenced by:  funssxp  5180  funforn  5240  funbrfvb  5347  funopfvb  5348  ssimaex  5365  fvco  5374  eqfunfv  5402  fvimacnvi  5413  unpreima  5424  respreima  5427  elrnrexdm  5438  elrnrexdmb  5439  ffvresb  5461  funresdfunsnss  5500  resfunexg  5518  funex  5520  elunirn  5545  smores  6057  smores2  6059  tfrlem1  6073  fundmfibi  6646  resunimafz0  10232  fclim  10678