Theorem funfn 4874

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 2037	. . 3 |- dom A = dom A
2	1	biantru 286	. 2 |- ( Fun A <-> ( Fun A /\ dom A = dom A))
3		df-fn 4848	. 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 1242   dom cdm 4288   Fun wfun 4839   Fn wfn 4840

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 1335  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-cleq 2030  df-fn 4848

This theorem is referenced by:  funssxp  5003  funforn  5056  funbrfvb  5159  funopfvb  5160  ssimaex  5177  fvco  5186  eqfunfv  5213  fvimacnvi  5224  unpreima  5235  respreima  5238  elrnrexdm  5249  elrnrexdmb  5250  ffvresb  5271  resfunexg  5325  funex  5327  elunirn  5348  smores  5848  smores2  5850  tfrlem1  5864