Theorem funfn 5226

Description: An equivalence for the function predicate. (Contributed by NM, 13-Aug-2004.)

Assertion

Ref	Expression
funfn	⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Proof of Theorem funfn

Step	Hyp	Ref	Expression
1		eqid 2170	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 300	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5199	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 186	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1348  dom cdm 4609  Fun wfun 5190   Fn wfn 5191

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 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-fn 5199

This theorem is referenced by:  funfnd  5227  funssxp  5365  funforn  5425  funbrfvb  5537  funopfvb  5538  ssimaex  5555  fvco  5564  eqfunfv  5596  fvimacnvi  5608  unpreima  5619  respreima  5622  elrnrexdm  5633  elrnrexdmb  5634  ffvresb  5657  funresdfunsnss  5697  resfunexg  5715  funex  5717  elunirn  5743  smores  6269  smores2  6271  tfrlem1  6285  funresdfunsndc  6483  fundmfibi  6913  resunimafz0  10755  fclim  11246