Theorem funfn 5285

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 5258	. 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 4660  Fun wfun 5249   Fn wfn 5250

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 5258

This theorem is referenced by:  funfnd  5286  funssxp  5424  funforn  5484  funbrfvb  5600  funopfvb  5601  ssimaex  5619  fvco  5628  eqfunfv  5661  fvimacnvi  5673  unpreima  5684  respreima  5687  elrnrexdm  5698  elrnrexdmb  5699  ffvresb  5722  funresdfunsnss  5762  resfunexg  5780  funex  5782  elunirn  5810  smores  6347  smores2  6349  tfrlem1  6363  funresdfunsndc  6561  fundmfibi  6999  resunimafz0  10905  fclim  11440