Theorem funfn 5363

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

Syntax hints:   ∧ wa 104   ↔ wb 105   = wceq 1398  dom cdm 4731  Fun wfun 5327   Fn wfn 5328

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 1498  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-fn 5336

This theorem is referenced by:  funfnd  5364  funssxp  5512  funforn  5575  funbrfvb  5695  funopfvb  5696  ssimaex  5716  fvco  5725  eqfunfv  5758  fvimacnvi  5770  unpreima  5780  respreima  5783  elrnrexdm  5794  elrnrexdmb  5795  ffvresb  5818  funiun  5837  funresdfunsnss  5865  resfunexg  5883  funex  5887  elunirn  5917  suppval1  6417  funsssuppss  6436  smores  6501  smores2  6503  tfrlem1  6517  funresdfunsndc  6717  fundmfibi  7180  resunimafz0  11141  fclim  11917  ausgrumgrien  16094