Theorem fnfun 3585

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 3193	. 2 |- (F Fn A <-> (Fun F /\ dom F = A))
2	1	pm3.26bi 322	1 |- (F Fn A -> Fun F)

Syntax hints:   -> wi 3   = wceq 956  dom cdm 3170  Fun wfun 3176   Fn wfn 3177

This theorem is referenced by:  fnrel 3586  funfni 3588  fneu 3592  fnco 3595  fnssresb 3599  fnex 3607  ffun 3629  f1ofun 3691  f1ocnv 3701  fvelimab 3765  fopabco 3832  fopabcos 3833  fconst3 3850  tfrlem2 3912  tfrlem4 3914  tfrlem11 3921  tz7.44-2 3929  tz7.44-3 3930  frfnom 3951  tz7.48-2 3957  tz7.49 3959  curry1 4098  inf0 4606  noinfep 4640  aceq3lem 4732  aceq3 4733  ac6lem 4754  zorn2lem6 4793  iundom 4812  alephfp 4900  uzrdgval 6302  0vfval 8225  vsfval 8254  ipasslem8 8497  sincolem 8665  cayleylem2 10410

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-fn 3193

Copyright terms: Public domain