Theorem funfn 4956

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 2054	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 290	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 4930	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 180	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 101   ↔ wb 102   = wceq 1257  dom cdm 4370  Fun wfun 4921   Fn wfn 4922

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1352  ax-ext 2036

This theorem depends on definitions:  df-bi 114  df-cleq 2047  df-fn 4930

This theorem is referenced by:  funssxp  5085  funforn  5138  funbrfvb  5241  funopfvb  5242  ssimaex  5259  fvco  5268  eqfunfv  5295  fvimacnvi  5306  unpreima  5317  respreima  5320  elrnrexdm  5331  elrnrexdmb  5332  ffvresb  5353  resfunexg  5407  funex  5409  elunirn  5430  smores  5935  smores2  5937  tfrlem1  5951  fclim  10009