Theorem fnfun 3571

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 3183	. 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 953  dom cdm 3160  Fun wfun 3166   Fn wfn 3167

This theorem is referenced by:  fnrel 3572  funfni 3574  fneu 3578  fnco 3581  fnssresb 3585  fnex 3593  ffun 3615  f1ofun 3676  f1ocnv 3686  fvelimab 3750  fopabco 3817  fopabcos 3818  fconst3 3835  tfrlem2 3897  tfrlem4 3899  tfrlem11 3906  tz7.44-2 3914  tz7.44-3 3915  frfnom 3936  tz7.48-2 3942  tz7.49 3944  curry1 4082  inf0 4578  noinfep 4612  aceq3lem 4704  aceq3 4705  ac6lem 4726  zorn2lem6 4765  iundom 4784  alephfp 4872  uzrdgval 6239  0vfval 8163  vsfval 8194  ipasslem8 8428  sincolem 8584  cayleylem2 10317

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 3183

Copyright terms: Public domain