Theorem funfn 5284

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 2193	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 302	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5257	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 187	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1364  dom cdm 4659  Fun wfun 5248   Fn wfn 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1460  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-fn 5257

This theorem is referenced by:  funfnd  5285  funssxp  5423  funforn  5483  funbrfvb  5599  funopfvb  5600  ssimaex  5618  fvco  5627  eqfunfv  5660  fvimacnvi  5672  unpreima  5683  respreima  5686  elrnrexdm  5697  elrnrexdmb  5698  ffvresb  5721  funresdfunsnss  5761  resfunexg  5779  funex  5781  elunirn  5809  smores  6345  smores2  6347  tfrlem1  6361  funresdfunsndc  6559  fundmfibi  6997  resunimafz0  10902  fclim  11437