Theorem funfn 5410

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 2238	. . 3 |- dom A = dom A
2	1	biantru 302	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 5383	. 2 |- ( A Fn dom A <-> ( Fun A /\ dom A = dom A ) )
4	2, 3	bitr4i 187	1 |- ( Fun A <-> A Fn dom A )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   = wceq 1402   dom cdm 4776   Fun wfun 5374   Fn wfn 5375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5383

This theorem is used by:  funfnd  5411  funssxp  5560  funforn  5625  funbrfvb  5746  funopfvb  5747  ssimaex  5767  fvco  5778  eqfunfv  5814  fvimacnvi  5826  unpreima  5836  respreima  5839  elrnrexdm  5850  elrnrexdmb  5851  ffvresb  5874  funiun  5893  funresdfunsnss  5921  resfunexg  5939  funex  5943  elunirn  5975  suppval1  6483  funsssuppss  6502  smores  6567  smores2  6569  tfrlem1  6583  funresdfunsndc  6783  fundmfibi  7256  resunimafz0  11296  fclim  12085  ausgrumgrien  16616