Theorem funfn 5218

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 2165	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 300	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 5191	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 186	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1343  dom cdm 4604  Fun wfun 5182   Fn wfn 5183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-fn 5191

This theorem is referenced by:  funfnd  5219  funssxp  5357  funforn  5417  funbrfvb  5529  funopfvb  5530  ssimaex  5547  fvco  5556  eqfunfv  5588  fvimacnvi  5599  unpreima  5610  respreima  5613  elrnrexdm  5624  elrnrexdmb  5625  ffvresb  5648  funresdfunsnss  5688  resfunexg  5706  funex  5708  elunirn  5734  smores  6260  smores2  6262  tfrlem1  6276  funresdfunsndc  6474  fundmfibi  6904  resunimafz0  10744  fclim  11235