Theorem funfn 4931

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 2040	. . 3 |- dom A = dom A
2	1	biantru 286	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A ) )
3		df-fn 4905	. 2 |- ( A Fn dom A <-> ( Fun A /\ dom A = dom A ) )
4	2, 3	bitr4i 176	1 |- ( Fun A <-> A Fn dom A )

Syntax hints:   /\ wa 97   <-> wb 98   = wceq 1243   dom cdm 4345   Fun wfun 4896   Fn wfn 4897

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-cleq 2033  df-fn 4905

This theorem is referenced by:  funssxp  5060  funforn  5113  funbrfvb  5216  funopfvb  5217  ssimaex  5234  fvco  5243  eqfunfv  5270  fvimacnvi  5281  unpreima  5292  respreima  5295  elrnrexdm  5306  elrnrexdmb  5307  ffvresb  5328  resfunexg  5382  funex  5384  elunirn  5405  smores  5907  smores2  5909  tfrlem1  5923  fclim  9815