Theorem funfn 5320

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 2207	. . 3 |- dom A = dom A
2	1	biantru 302	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 5293	. 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 1373   dom cdm 4693   Fun wfun 5284   Fn wfn 5285

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 1473  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-fn 5293

This theorem is referenced by:  funfnd  5321  funssxp  5465  funforn  5527  funbrfvb  5644  funopfvb  5645  ssimaex  5663  fvco  5672  eqfunfv  5705  fvimacnvi  5717  unpreima  5728  respreima  5731  elrnrexdm  5742  elrnrexdmb  5743  ffvresb  5766  funiun  5784  funresdfunsnss  5810  resfunexg  5828  funex  5830  elunirn  5858  smores  6401  smores2  6403  tfrlem1  6417  funresdfunsndc  6615  fundmfibi  7066  resunimafz0  11013  fclim  11720