Theorem funfn 5272

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 2189	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 302	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5245	. 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 4651  Fun wfun 5236   Fn wfn 5237

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 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-fn 5245

This theorem is referenced by:  funfnd  5273  funssxp  5411  funforn  5471  funbrfvb  5586  funopfvb  5587  ssimaex  5605  fvco  5614  eqfunfv  5646  fvimacnvi  5658  unpreima  5669  respreima  5672  elrnrexdm  5683  elrnrexdmb  5684  ffvresb  5707  funresdfunsnss  5747  resfunexg  5765  funex  5767  elunirn  5795  smores  6325  smores2  6327  tfrlem1  6341  funresdfunsndc  6539  fundmfibi  6976  resunimafz0  10858  fclim  11349