Theorem funfn 5228

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

Syntax hints:   ∧ wa 103   ↔ wb 104   = wceq 1348  dom cdm 4611  Fun wfun 5192   Fn wfn 5193

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 1442  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-fn 5201

This theorem is referenced by:  funfnd  5229  funssxp  5367  funforn  5427  funbrfvb  5539  funopfvb  5540  ssimaex  5557  fvco  5566  eqfunfv  5598  fvimacnvi  5610  unpreima  5621  respreima  5624  elrnrexdm  5635  elrnrexdmb  5636  ffvresb  5659  funresdfunsnss  5699  resfunexg  5717  funex  5719  elunirn  5745  smores  6271  smores2  6273  tfrlem1  6287  funresdfunsndc  6485  fundmfibi  6916  resunimafz0  10766  fclim  11257