Theorem funfn 4955

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 2082	. . 3 ⊢ dom 𝐴 = dom 𝐴
2	1	biantru 296	. 2 ⊢ (Fun 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
3		df-fn 4929	. 2 ⊢ (𝐴 Fn dom 𝐴 ↔ (Fun 𝐴 ∧ dom 𝐴 = dom 𝐴))
4	2, 3	bitr4i 185	1 ⊢ (Fun 𝐴 ↔ 𝐴 Fn dom 𝐴)

Syntax hints:   ∧ wa 102   ↔ wb 103   = wceq 1285  dom cdm 4365  Fun wfun 4920   Fn wfn 4921

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-fn 4929

This theorem is referenced by:  funssxp  5085  funforn  5138  funbrfvb  5242  funopfvb  5243  ssimaex  5260  fvco  5269  eqfunfv  5296  fvimacnvi  5307  unpreima  5318  respreima  5321  elrnrexdm  5332  elrnrexdmb  5333  ffvresb  5354  resfunexg  5408  funex  5410  elunirn  5431  smores  5935  smores2  5937  tfrlem1  5951  fundmfibi  6438  fclim  10260