Theorem funfn 5148

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

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1331  dom cdm 4534  Fun wfun 5112   Fn wfn 5113

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 1425  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-fn 5121

This theorem is referenced by:  funfnd  5149  funssxp  5287  funforn  5347  funbrfvb  5457  funopfvb  5458  ssimaex  5475  fvco  5484  eqfunfv  5516  fvimacnvi  5527  unpreima  5538  respreima  5541  elrnrexdm  5552  elrnrexdmb  5553  ffvresb  5576  funresdfunsnss  5616  resfunexg  5634  funex  5636  elunirn  5660  smores  6182  smores2  6184  tfrlem1  6198  funresdfunsndc  6395  fundmfibi  6820  resunimafz0  10567  fclim  11056