Theorem funfn 5153

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 2139	. . 3 |- dom A = dom A
2	1	biantru 300	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 5126	. 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 1331   dom cdm 4539   Fun wfun 5117   Fn wfn 5118

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

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-fn 5126

This theorem is referenced by:  funfnd  5154  funssxp  5292  funforn  5352  funbrfvb  5464  funopfvb  5465  ssimaex  5482  fvco  5491  eqfunfv  5523  fvimacnvi  5534  unpreima  5545  respreima  5548  elrnrexdm  5559  elrnrexdmb  5560  ffvresb  5583  funresdfunsnss  5623  resfunexg  5641  funex  5643  elunirn  5667  smores  6189  smores2  6191  tfrlem1  6205  funresdfunsndc  6402  fundmfibi  6827  resunimafz0  10574  fclim  11063