Theorem funfn 5089

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

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1299  dom cdm 4477  Fun wfun 5053   Fn wfn 5054

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

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-fn 5062

This theorem is referenced by:  funfnd  5090  funssxp  5228  funforn  5288  funbrfvb  5396  funopfvb  5397  ssimaex  5414  fvco  5423  eqfunfv  5455  fvimacnvi  5466  unpreima  5477  respreima  5480  elrnrexdm  5491  elrnrexdmb  5492  ffvresb  5515  funresdfunsnss  5555  resfunexg  5573  funex  5575  elunirn  5599  smores  6119  smores2  6121  tfrlem1  6135  funresdfunsndc  6332  fundmfibi  6755  resunimafz0  10415  fclim  10902