Theorem funfn 4961

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 2082	. . 3 |- dom A = dom A
2	1	biantru 296	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 4935	. 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 1285   dom cdm 4371   Fun wfun 4926   Fn wfn 4927

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 1379  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-fn 4935

This theorem is referenced by:  funssxp  5091  funforn  5144  funbrfvb  5248  funopfvb  5249  ssimaex  5266  fvco  5275  eqfunfv  5302  fvimacnvi  5313  unpreima  5324  respreima  5327  elrnrexdm  5338  elrnrexdmb  5339  ffvresb  5360  resfunexg  5414  funex  5416  elunirn  5437  smores  5941  smores2  5943  tfrlem1  5957  fundmfibi  6448  fclim  10271