Theorem fnfun 2721

Description: A function with domain is a function.

Assertion

Ref	Expression
fnfun	⊢ (F Fn A → Fun F)

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 2433	. 2 ⊢ (F Fn A ↔ (Fun F ∧ dom F = A))
2	1	pm3.26bd 259	1 ⊢ (F Fn A → Fun F)

Syntax hints:   → wi 2   = wceq 1091  dom cdm 2410  Fun wfun 2416   Fn wfn 2417

This theorem is referenced by:  fnrel 2722  funfni 2724  fneu 2728  fnssres 2734  fnex 2740  ffun 2754  f1ofun 2802  f1ocnv 2811  fvelrn 2883  tfrlem2 2950  tfrlem4 2952  tfrlem11 2959  tz7.44-2 2967  tz7.44-3 2968  frfnom 2989  tz7.48-2 2995  tz7.49 2997  inf0 3457  aceq3lem 3555  aceq3 3556  ac6lem 3575  zornlem6 3608  uzrdgval 4657

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198  df-fn 2433

metamath.org