Theorem funfn 5289

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 2196	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 302	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5262	. 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 4664  Fun wfun 5253   Fn wfn 5254

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 1463  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-fn 5262

This theorem is referenced by:  funfnd  5290  funssxp  5430  funforn  5490  funbrfvb  5606  funopfvb  5607  ssimaex  5625  fvco  5634  eqfunfv  5667  fvimacnvi  5679  unpreima  5690  respreima  5693  elrnrexdm  5704  elrnrexdmb  5705  ffvresb  5728  funresdfunsnss  5768  resfunexg  5786  funex  5788  elunirn  5816  smores  6359  smores2  6361  tfrlem1  6375  funresdfunsndc  6573  fundmfibi  7013  resunimafz0  10940  fclim  11476